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.
