What is wrong with this simple proof of P=NP?

Question

Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiabilty problem. Given an instance of clauses where each clause has three literals, is there a set of literals such that each clause contains exactly one literal from the set. $X3SAT$ is NP-Complete even when the instance is monotone and linear. Monotone means all literals are positive. Linear means no two clauses share more than one variable in common.

The algorithm I describe is basically Davis, Putnam, Logeman, Loveland ($DPLL$) with fixed variable order and without unit clause propogation or pure literal elimination. The algorithm also has a simple Conflict Driven Clause Learning ($CDCL$) procedure. This $CDCL$ procedure is key to the proof.

Order the literals in each clause lexicographically. Then, order the clauses lexicographically. Reorder the literals based on the first clause the literal appears in. This instance has $n=13$ variables and $m=10$ clauses. The clauses are in lexicographical order:

$\quad(a,c,k)(a,i,l)(b,j,m)(c,d,e)(c,f,g)(e,g,k)(e,h,l)(f,k,l)(g,j,l)(i,k,m)$

The order the literals first appear in a clause: $\quad a,c,k,i,l,b,j,m,d,e,f,g,k,h,l,j,i,m$

Algorithm description:

1) Choose the lowest order clause that has not been satisfied. Choose the lowest order unset literal in this clause and set it to true.

2) Process all clauses containing this true literal and set any unset literals in these clauses to false. Keep a list of the literals set to false by this true literal.

3) Reduce any learned clauses. If there are any unit learned clause that haven't already been listed, add the inverse of these unit clauses to the list of literals set to false on step 2.

4) They only way a conflict can occur is when all literals in a clause are set to false. If there are no such clauses go to step 1. Else, find the lowest order clause with all literals set to false. Determine which true literals forced the literals in this clause to be false. Create a disjunction of the inverses of these true literals. Note, this learned clause won't have more than three literals.

5) Add the new learned clause to the set of learned clauses and restart. If there are unit learned clauses when restarting, assume the inverses of these units clauses are set false. These starting unit learned clauses should be added to the list of literals set to false on the first step.

Example:

Set $a$ to true in $(a,c,k)$. Literals forced to be false are $c,k,i,l$.

Set $b$ to true in $(b,j,m)$. Literals forced to be false are $j,m$.

Set $d$ to true in $(c,d,e)$. Literal forced to be false is $e$.

Set $f$ to true in $(c,f,g)$. Literal forced to be false is $g$.

All the literals in $(e,g,k)$ are false.

$k$ was set false when $a$ was set true.

$e$ was set false when $d$ was set true.

$g$ was set false when $f$ was set true.

Create the learned clause $(\bar a \lor \bar d \lor \bar f)$ and restart.

Set $a$ to true in $(a,c,k)$. Literals forced to be false are $c,k,i,l$.

Set $b$ to true in $(b,j,m)$. Literals forced to be false are $j,m$.

Set $d$ to true in $(c,d,e)$. Literal forced to be false are $e,f$.

$f$ is set to false because of the learned clause.

$(f,k,l)$ is a new conflict.

$k$ and $l$ were set false when $a$ was set true.

$f$ was set false when $d$ was set true.

Create the learned clause $\quad(\bar a \lor \bar d)$.

Repeating this process eventually creates the following learned clauses;

$\quad(\bar a \lor \bar d \lor \bar f)(\bar a \lor \bar d)(\bar a \lor \bar b)(\bar a \lor \bar j)(\bar a \lor \bar e)(\bar a)(\bar c)(\bar k)$

The learned clauses $(\bar a)(\bar c)(\bar k)$ prove the clause $(a,c,k)$ can't be satisfied. The instance is unsatisfiable.

If an instance is unsatisfiable, this algorithm must find a conflict before it processes all $m$ of the clauses. A conflict generates an unique learned clause. There are at most $O(n^3)$ unique learned clauses and each learned clause requires processing fewer than $m$ clauses. This algorithm can determine if a monotone, linear $X3SAT$ instance is unsatisfiable in $O(m \cdot n^3)$ steps.

What is wrong with this proof?

At first, I wondered if the method for generating learned clauses was sound. Now, I think I can show all the learned clauses can be derived using resolution. An $X3SAT$ instance can be converted to a $2+SAT$ instance using this transformation:

$\quad (a,b,c) = (a \lor b \lor c)(\bar a \lor \bar b)(\bar a \lor \bar c)(\bar b \lor \bar c)$

The learned clause $(\bar a \lor \bar d \lor \bar f)$ can be derived from the $X3SAT$ clauses $(a,c,k)(a,i,l)(c,d,e)(c,f,g)(e,g,k)$. Converting to $2+SAT$ gives an expression that includes the clauses $(e \lor g \lor k)(\bar d \lor \bar e)(\bar f \lor \bar g)(\bar a \lor \bar k)$. Resolving these clauses gives $(\bar a \lor \bar d \lor \bar f)$. Transforming the clause $(f,k,l)$ allows us to resolve $(f \lor k \lor l)(\bar a \lor \bar k)(\bar a \lor \bar l)$ to get $(\bar a \lor f)$. Resolving $(\bar a \lor f)$ with $(\bar a \lor \bar d \lor \bar f)$ gives $(\bar a \lor \bar d)$. The resolution derivation can get quite long when numerous learned clauses are involved in the derivation. This $CDCL$ procedure can be easily modified to include unit clause resolution and can be modified to apply to $3SAT$.

---

There seems to be some confusion because I combine $X3SAT$ with $3SAT$. To eliminate the confusion, I will show how this algorithm can be used to solve Monotone 3SAT instances.

The monotone in monotone $3SAT$ has a different definition than the monotone in monotone $X3SAT$. Monotone $3SAT$ means every clause has all positive literals or all negative literals. I will use "positive clause" for clauses with all positive literals and "negative clause" for clauses with all negative literals.

Assume we have a monotone $X3SAT$ instance as above. Convert this instance to monotone $3SAT$ using the following tranformation:

$\quad (a,b,c) = (a \lor b \lor c)(\bar a \lor \bar b)(\bar a \lor \bar c)(\bar b \lor \bar c)$

The transfomed instance will have positive 3-clauses and negative 2-clauses. The algorithm above will need minor changes. We only need to order the positive clauses. The first step becomes:

1) Choose the lowest order positive clause. This might be a unit clause. Set the lowest order unassigned variable in this clause to true. The instance is satisfiable if there are no positive clauses. All remaining clauses have at least one negated literal. Assuming all the unset variables are false will satisfy all remaining clauses.

The second and third steps above get combined into one step.

2) Reduce the instance using the latest positive decision variable. Propagate any negative unit clauses. Keep a list of all negative unit clause that haven't already been listed. Do not propagate positive unit clauses.

The other steps remain the same as above. As before, any conflict can be shown to be caused by no more than three positive decision variables.

I removed the section about propagating positive unit clauses. At the moment, I can't show the learned clause created by propagating positive unit clauses can be created using resolution.

Answer 1

The monotone version of X3SAT that your proof is based on has the nice property that setting a literal false in one clause will never cause the negation of that literal to be true in another, which means you can say

The only way a conflict can occur is when all literals in a clause are set to false.

and it will be true because forcing two literals false in one clause will never force their two negations true in another, since there are no negated variables in the formula.

The problems come when you start learning clauses. First, you can't just learn a disjunction like $(\bar a \lor \bar d \lor \bar f)$ because that's not a X3SAT clause, it's a 3CNF clause. You'll have to convert this normal 3CNF clause to a set of equivalent X3SAT clauses, e.g. using Schaefer's method. This means more clauses, but it's a polynomial blowup so you're still OK.

The second problem is unfortunately a killer for your proof. The learned X3SAT clauses will have negated variables in them, making the formula no longer monotone. With a non-monotone formula you can no longer rely on all-false literals being the only kind of conflict clause; now you must worry about clauses with more than one true literal as they can now be produced by setting two other literals false elsewhere. Your proof has no provision for handling these unsatisfied clauses.

Answer 2

I found a flaw in my proof. There are situations were this algorithm will not find satisfying assignments.

Assume a set of clauses like:

$\quad(a,b,c)(d,e,f)(g,h,i)(j,k,l)(m,n,o)(b,k,n)(e,h,m)$

The clauses $(a,b,c)(j,k,l)(m,n,o)(b,k,n)$ would create the learned clause $(\bar a \lor \bar j \lor \bar m)$ from the conflict clause $(b,k,n)$.

Now assume we set $a$, $d$, $g$, and $j$ true creating the conflict clause $(e,h,m)$.

$e$ was set false when $d$ was set true.

$h$ was set false when $g$ was set true.

$m$ was set false because both $a$ and $j$ were set true. But, my algorithm says $m$ was set false when only $j$ was set true. My algorithm would create the learned clause $(\bar d \lor \bar g \lor \bar j)$. It should have created the learned clause $(\bar a \lor \bar d \lor \bar g \lor \bar j)$.

Now assume the $X3SAT$ instance has only one satisfying assignment where $a$ is false and $d$, $g$, and $j$ are true. My algorithm would never find this satisfying assignment.

I was correct to say this algorithm can determine if a monotone $X3SAT$ instance is unsatisfiable in $O(m \cdot n^3)$ steps. An algorithm that always returns "unsatisfiable" can do it in one step.