0
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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)$$ ? $\endgroup$ – Nicholas Viggiano Oct 21 '19 at 13:03
  • $\begingroup$ @NicholasViggiano, good question, thanks! I didn't see such a case, let's try if a solution similar to a Horn formula works... $\endgroup$ – Serge Rogatch Oct 21 '19 at 13:34
  • $\begingroup$ @NicholasViggiano, huge thanks to you, we've found how to solve such cases and I'm editing the question. $\endgroup$ – Serge Rogatch Oct 21 '19 at 14:05
  • $\begingroup$ @NicholasViggiano, please, see my update #2. $\endgroup$ – Serge Rogatch Oct 21 '19 at 14:21
  • $\begingroup$ 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? $\endgroup$ – Nicholas Viggiano Oct 21 '19 at 15:45
0
$\begingroup$

No. 3SAT is the lowest level of k-SAT to which any set of strings can be reduced. What people have consistently failed to realize is that SAT is an expression of a set of strings of some n length. Ergo, every set of strings has a corresponding n-SAT expression. Any n-SAT expression can be reduced to a k < n k-SAT expression in polynomial time. 2SAT however lacks sufficient structure to capture the set of strings in a tractable expression. This is not to say that individual n-SAT expressions cannot be reduced to 2SAT; just that not all can be so expressed. See arxiv.org/abs/cs/0205064.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.