Definition

In this post, I will show a polynomial-time computable function that maps a CHF formula f to a 3-CNF formula f’, such that f is satisfiable iff f’ is satisfiable. But some definition first:

• CNF (conjunctive normal form) is kind of “simplest” form of a logical formula - an AND of ORs. It is AND of multiple clauses where each is OR of multiple literals. Example: (a OR b OR c) AND ((NOT b) OR c). 3-CNF simply means there are 3 literals in each clause.
• Literal is (a) , (NOT b) in the above example. Notice that it’s different from variables, which are a and b respectively.
• Satisfiable means there is a way to set true/false value to each variable in the logical formula, such that the formula evaluate to true.

Convert clauses

Okie. So the basic strategy is to convert each clause in CNF to equivalent 3-CNF clauses. Notice that clause in CNF can has arbitrary length, how can we do this conversion? We add new variables. Let’s take an example:

2-literal clause:

Transform $latex (z_1 \vee z_2)$ to $latex (z_1 \vee z_2 \vee y) \wedge (z_1 \vee z_2 \vee \bar y)$ The truth value of result clauses depends only on $latex (z_1 \vee z_2)$. Since y or $latex \bar y$ must be false, hence making the corresponding clause value depends on $latex (z_1 \vee z_2)$. For the other clause, its value is true hence we don’t need to care for that in the overall result.

1-literal clause:

Transform $latex (z_1 \vee z_2)$ to $latex (z_1 \vee \bar y_1 \vee y_2) \wedge (z_1 \vee y_1 \vee \bar y_2) \wedge (z_1 \vee y_1 \vee y_2) \wedge (z_1 \vee \bar y_1 \vee \bar y_2) \wedge $ we introduce 2 new variables in the result clause which create 4 combinations of its literals. However since it’s OR operator, only 1 of the four clauses can be false no matter how we assign true values to the new variables. Hence, that clause (which value depends on z1) will decide the truth value of the whole result clauses.

3-literal clause:

we don’t have to do anything in this case.

more than 3 literal clause:

we break the clause into 3-literals chunks using new variables. Notice the first transformation in the above proof. We set $latex y_3 = z_1 \vee z_2 \vee z_3 \vee z_4$. If the first line is true, then the second line is true. There are two cases for the second line: if y3 is true then both clauses are true. Otherwise the complement of y3 satisfy the first clause, while either z5 or z6 is true, making second clause satisfied. In the other direction, we have the second line is true. So there are two cases: if y3 is true, then first line is obviously true. Otherwise either z5 or z6 is true, hence the first line is also true.

This is an ongoing series of posts where I try to learn a concept by writing blog post about it. The screen shots from this post is taken from the Algorithm course in Udacity.