# A reduction of 3-CNF down to 2-CNF for boolean satisfiability

Could you please review the following candidate solution for the boolean satisfiability problem?

It is known that 2-CNF has a polynomial solution.

Now consider we have a 3-CNF (AFAIK, it's proven that every boolean formula can be reduced to 3-CNF in polynomial time).

If no 2 clauses have the same pair of variable (like a1 and a2 in one clause, and -a1 and a2 in another clause), then the formula can be simply assigned true/false values for the variables in the middle of each link of the chain, like: (a1 v a2 v a3)(-a3 v -a4 v a5)etc. - here we simply assign a2=1 and a4=0, and no matter what the values of the other variables are, the formula is satisfiable already.

Now consider some 2 clauses have the same pair of variables, possibly negated. In each step of the program we find such 3-clauses and transform them into implicative 2-clauses as follows.

(a1 v a2 v a3)(a2 v a3 v -a4) and (a1 v -a2 v -a3)(-a2 v -a3 v -a4) - here a2 and a3 is the pair and we transform this into 2-CNF with replacements x = (a2 v a3) and x = (-a2 v -a3) respectively.

Next, consider a2 and a3 participate in 3-CNF as follows: (a1 v a2 v -a3)(-a2 v a3 v a4) Then we can replace x=a2 v -a3 and y=-a2 v a3. We get 2-CNF (a1 v x)(y v a4) that can be transformed into implicative form. However, it lacks 4 more implicative relations between x, -x, y and -y. Let's show how these are related. Here + denotes a XOR operation.

a2 v -a3 | -a2 v a3 | a2 | a3 | x+y | x*y |
-------------------------------------------
1           1       0    0    0     1
0           1       0    1    1     0
1           0       1    0    1     0
1           1       1    1    0     1


From the truth table, we can infer that x*y = x+y+1

Consequently,

x * -y = -y
y * -y =  0
-x * x =  0
-x * y = -x
-x * -y = 0


From the first and the fourth equations above we can infer 4 implicative clauses in total:

x * -y = -y   =>  (-y -> x) and (y -> -x)
-x * y = -x   =>  (-x -> y) and (-y -> x)


By analogy, we can reduce 3-CNF clauses into 2-CNF implicative clauses for (a1 v a2 v a3)(-a2 v a3 v a4) replacing x=(a2 v a3) and y=(-a2 v a3), and for (a1 v -a2 v -a3)(a1 v a2 v a3) replacing x=(-a2 v -a3) and y=(a2 v a3).

So the problem of boolean satisfiability seems to have been reduced polynomially into 2-CNF BSAT problem that has a polynomial solution in its turn.

UPDATE: let me finish showing how case x=(a2 v a3) and y=(-a2 v a3), and case x=(-a2 v -a3) and y=(a2 v a3) get handled.

Truth table #2 for x=(a2 v a3) and y=(-a2 v a3):

a2 v a3 | -a2 v a3 | a2 | a3 | x+y | x*y |
-------------------------------------------
0          1       0    0    1     0
1          1       0    1    0     1
1          0       1    0    1     0
1          1       1    1    0     1


Equations:

x*y =  a3 }
} => x*y = x+y+1
x+y = -a3 }

x * -y = -y
y * -y = 0
-x * x = 0
-x * y = -x
-x * -y = 0


Consequences:

x * -y = -y   =>  (-y -> x) and (-x -> y)
-x * y = -x   =>  (-x -> y) and (x -> -y)


Finally, for case x=(-a2 v -a3) and y=(a2 v a3):

Truth table #3:

-a2 v -a3 | a2 v a3 | a2 | a3 | x+y | x*y |
-------------------------------------------
1          0       0    0    1     0
1          1       0    1    0     1
1          1       1    0    0     1
0          1       1    1    1     0


Equations:

x * y = x + y + 1
x * -y = -y
y * -y = 0
-x * x = 0
-x * y = -x
-x * -y = 0


Consequences:

x * -y = -y   =>  (-y -> x) and (-x -> y)
-x * y = -x   =>  (-x -> y) and (x -> -y)


UPDATE2:

After the above transformations, no pairs stay in the formula, e.g.

(a1 v a2 v a3)(-a1 v a4 v a5)(-a2 v -a4 v a7)(-a3 v -a5 v -a7).

In general, this case is (a1 v a2 v ...)(-a1 v a3 v ...).... So we take two 3-clauses where the same variable appears straight and negated, and then we substitute x = a1 v a2 and y = -a1 v a3.

Truth table:

a1 v a2 | -a1 v a3 | a1 | a2 | a3 | x*y | x+y |
-----------------------------------------------
0    |     1    | 0  | 0  | 0  |  0  |  1  |
0    |     1    | 0  | 0  | 1  |  0  |  1  |
1    |     1    | 0  | 1  | 0  |  1  |  0  |
1    |     1    | 0  | 1  | 1  |  1  |  0  |
1    |     0    | 1  | 0  | 0  |  0  |  1  |
1    |     1    | 1  | 0  | 1  |  1  |  0  |
1    |     0    | 1  | 1  | 0  |  0  |  1  |
1    |     1    | 1  | 1  | 1  |  1  |  0  |


We get similar equations as for pairs:

x  *  y = x + y + 1
x  * -y = -y
-x *  y = -x
-x * -y = 0


Consequences:

x  * -y = -y   =>   (-y -> x) and (-x -> y)
-x *  y = -x   =>   (-x -> y) and (-y -> x)


Update3: If no variable appears both straight in one 3-clause and negated in another 3-clause, then we simply assign to each variable true if it appears straight only and false if it appears negated only.

So it seems that P=NP.

• In your no-pairs case, what happens with a formula like $$(a_1 \vee a_2 \vee a_3) \wedge (\lnot a_1 \vee a_4 \vee a_5) \wedge (\lnot a_2 \vee \lnot a_4 \vee a_7) \wedge (\lnot a_3 \vee \lnot a_5 \vee \lnot a_7)$$ ? Oct 21 '19 at 13:03
• @NicholasViggiano, good question, thanks! I didn't see such a case, let's try if a solution similar to a Horn formula works... Oct 21 '19 at 13:34
• @NicholasViggiano, huge thanks to you, we've found how to solve such cases and I'm editing the question. Oct 21 '19 at 14:05
• @NicholasViggiano, please, see my update #2. Oct 21 '19 at 14:21
• Sorry, I am still not clear on what happens with formulas like $$(a_1 \vee a_2 \vee a_3) \wedge (\lnot a_1 \vee \lnot a_2 \vee a_4) \wedge (a_2 \vee \lnot a_3 \vee a_4)$$ assuming $a_4$ is used again later. Do not your $x$ and $y$ trip over each other? Oct 21 '19 at 15:45