Conflict Clusters – Another P=NP Proof
Exactly 1 in 3 SAT ($X3SAT$) is a variation of the Boolean Satisfiability 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.
Any XSAT instance can easily be made monotone and linear. Replace any negated literal, like $\bar{a}$, with a positive literal, $a0$, and add the clause $(a,a0)$.
A monotone X3SAT instance can be made linear with this reduction rule:
$(a,b,c) \cap (a,b,d) \cap X() \rightarrow (a,b,c) \cap X(c \leftarrow d)$ where $X()$ is an XSAT instance.
$c=d$. Replace all occurrences of $d$ with $c$ and remove duplicate clauses.
There is also a subsumption reduction rule:
$(a,b) \cap (a,b,c) \cap X() \rightarrow (a,b) \cap X(False \leftarrow c)$
$c$ must be False. Remove $c$ from all clauses and remove duplicate clauses.
The algorithm I describe is basically Davis, Putnam, Logeman, Loveland with fixed clause order and unit clause propagation. Instead of using Conflict Driven Clause Learning, this algorithm creates assignment clauses which are lists of satisfying assignments to conflict clusters.
Assume we start with a monotone, linear instance of X2SAT and X3SAT clauses. This algorithm sets one variable to true and then processes all clauses with this variable and sets the other variables in these clauses to false. This means a conflict can only occur when all variables in a clause are set false.
A conflict cluster is a set of clauses and a partial variable assignment that causes a conflict. One clause is a conflict clause where all literals are false. The other clauses are satisfied by the current partial assignment and share a variable with the conflict clause. If the conflict cluster is made up of linear and monotone X3SAT clauses, then the smallest conflict cluster has four clauses. No conflict cluster of X3SAT clauses requires more than four clauses. These four clauses can have 7, 8, or 9 variables. Conflict clusters with 7 variables have three satisfying assignments. Those with 8 variables have six satisfying assignments, and those with 9 variables have twelve.
This is an example of a conflict cluster with 7 variables and three satisfying assignments:
The partial assignment is $a, \bar{b}, \bar{x}, \bar{c}, \bar{y}, \bar{d}, \bar{z}$:
$(A,b,x) \cap (A,c,y) \cap (A,d,z) \cap (x,y,z)$
This conflict cluster has three satisfying assignments:
$b, c, z, \bar{a}, \bar{x}, \bar{y}, \bar{d}$
$b, y, d, \bar{a}, \bar{x}, \bar{c}, \bar{z}$
$x, c, d, \bar{a}, \bar{b}, \bar{y}, \bar{z}$
We use these satisfying assignments to create an assignment clause:
$(bcz \bar{a} \bar{x} \bar{y} \bar{d}, bdy \bar{a} \bar{x} \bar{c} \bar{z}, xcd \bar{a} \bar{b} \bar{y} \bar{z})$
Assignment clauses are treated like XSAT clauses. Instead of choosing one literal to be true, we choose one of the mutually exclusive assignments to be true.
Assignment clauses can become unit clauses. For example, if we had a partial assignment where $z$ is true, then $bcz \bar{a} \bar{x} \bar{y} \bar{d}$ would be the only consistent assignment left in this assignment clause.
If the conflict clause is an X2SAT clause then the conflict cluster only requires three clauses. An X2SAT conflict cluster can have from 3 to 6 variables An X2SAT conflict cluster with 3 variables has no satisfying assignments:
Partial assignment: $a, \bar{b}, \bar{c}$
$(a,b) \cap (a,c) \cap (b,c)$
An X2SAT conflict cluster with 4 variables has 1 satisfying assignment, with 5 variables has 2 satisfying assignments, and with 6 variables has 4 satisfying assignments.
This algorithm only backtracks when it finds a conflict cluster. There can't be more than $O(m^4)$ conflict clusters where $m$ is the number of clauses. This algorithm must terminate in a polynomial number of steps.
In a standard $DPLL$ algorithm with fixed variable order the first step is to order the variables. Then choose the highest order variable to be the "choice variable" and set it to false. If this leads to a contradiction then we backtrack and set the choice variable to true. If all choices for a choice variable lead to contradition then we backtrack to a previous choice variable.
The first step of this algorithm is to order the clauses. Clauses are treated like variables except they can have three different values instead of two. We will the choose a "choice clause" and set the lowest order variable in the clause to true. If this leads to a contradiction then we backtrack and set the next lowest order variable in the choice clause to true. If all the choices lead to contradiction, then we backtrack to a previous choice clause.
This algorithm has a non-linear backtracking method I will describe below.
Algorithm:
Choose the highest order unsatisfied clause. This is a decision clause.
Choose the lowest order unassigned variable in this clause that hasn’t already been tried and set it true. If the clause is a assignment clause then choose the lowest order satisfying assignment that hasn’t already been tried. Process each true variable in an assignment one variable at a time. The first true variable processed from the assignment satisfies the highest order clause in the conflict cluster. The second true variable processed would satisfy the next highest order clause in the conflict cluster, etc.
Process all clauses containing the newly set true variable and set all other variables in these clauses to false. Remove assignments from assignment clauses that are inconsistent with the current partial assignment.
If there are no conflicts and no unit clauses go to step 1.
If there are no conflicts then choose the highest order unit clause. Go to step 2.
Process the conflict. See below.
Backtrack to the highest order decision clause where the partial assignment is inconsistent with all of the new conflict cluster's satisfying assignments.
Undo the decisions made below this clause. Increment this clause to the next unset and untried variable/assignment that is consistent with at least one of the new conflict cluster assignments. Set this variable true and go to step 3.
If there are no untried variables/assignments consistent with the new conflict cluster assignments then backtrack to the previous decision clause and go to 8. If there is no previous decision clause the instance is unsatisfiable.
Processing a conflict cluster:
Setting a variable true may create multiple conflicts clusters. Choose the conflict cluster with the highest order clauses.
Create a list of all of the satisfying assignments to the conflict cluster. Apply each assignment against the entire instance. Process any unit clauses. If the assignment causes a conflict, then remove it from the list. If all assignments are removed then the instance is unsatisfiable. This is a common way of showing an instance is unsatisfiable.
If there is only one satisfying assignment left in the list then this assignment is forced. Reduce the instance with the assignment and restart.
If a variable is true in every assignment or false in every assignment then this assignment is forced. Reduce the instance with the assignment and restart.
Order the assignments in the list based on satisfying the clauses in the conflict cluster in order. Order the assignments from the lowest clause order assignment to the highest clause order assignment.
Create an assignment clause with the remaining satisfying assignments. Add this clause just before the highest order clause in the conflict cluster.
More than one conflict cluster can have the same highest order clause. When this happens, order the assignment clauses based on the order of the conflict clusters. Conflict clusters can always be uniquely ordered based on the order of the clauses in the conflict cluster.
Example:
The instance below has 19 variables and 13 clauses. This algorithm finds one of the four satisfying assignments after processing one conflict cluster and backtracking once. I deliberately ordered the clauses “badly” so I can show how backtracking works.
$(c,k,q) \cap (d,m,r) \cap (a,b,c) \cap (a,d,e) \cap (f,g,h) \cap (b,d,g) \cap (i,j,k) \cap (i,l,m) \cap (n,o,p) \cap (j,l,o) \cap (h,p,s) \cap (q,r,s) \cap (k,n,r)$
The first conflict occurs when the choice clause $(i,j,k)$ is processed.
$$\begin{array} {|r|r|r|} \hline \text{Choice Clause} & \text{Value} & \text{Variables Assigned}\\ \hline (c,k,q) & c & c \bar{k} \bar{q} \bar{a} \bar{b}\\ \hline (d,m,r) & d & d \bar{m} \bar{r} \bar{e} \bar{g} s \bar{h} \bar{p} f n \bar{o}\\ \hline (i,j,k) & i & (j,l,o) \text{ is a conflict clause}\\ \hline \end{array}$$
$(I,j,k)(I,l,m)(N,o,p)(j,l,o)$ is a conflict cluster with 8 variables and six satisfying assignments. Of these six satisfying assignments, only two don't cause conflicts with the rest of the instance. For example, $i o \bar{j} \bar{k} \bar{l} \bar{m} \bar{n} \bar{p}$ satisfies the conflict cluster, but, creates unit clauses that force $r,c,e,g$ to be true. This creates the conflict cluster $(f,G,h)(n,O,p)(h,p,s)(q,R,s)$.
The two remaining satisfying assignments are:
$j m n \bar{i} \bar{k} \bar{l} \bar{o} \bar{p}$
$k m o \bar{i} \bar{j} \bar{l} \bar{n} \bar{p}$
Assignment clause ordered by lowest order assignment, highest order assignment:
$(j m n \bar{i} \bar{k} \bar{l} \bar{o} \bar{p}, k m o \bar{i} \bar{j} \bar{l} \bar{n} \bar{p})$
Order this assignment clause before the first clause in the conflict cluster, $(i,j,k)$:
$(c,k,q) \cap (d,m,r) \cap (a,b,c) \cap (a,d,e) \cap (f,g,h) \cap (b,d,g) \cap (j m n \bar{i} \bar{k} \bar{l} \bar{o} \bar{p}, k m o \bar{i} \bar{j} \bar{l} \bar{n} \bar{p}) \cap (i,j,k) \cap (i,l,m) \cap (n,o,p) \cap (j,l,o) \cap (h,p,s) \cap (q,r,s) \cap (k,n,r)$
Backtracking:
Since $m,i,l,p$ all have the same value in both assignments, the algorithm says to reduce the instance with these variable assignments and restart. Instead, I will show how we would backtrack.
Both satisfying conflict cluster assignments are inconsistent with $m$ being False. This means $(d,m,r)$ is the highest order choice clause that conflicts with all of the conflict cluster's satisfying assignments.
Backtrack to $(d,m,r)$ and increment the value to $m$ being true. This is consistent with $j m n \bar{i} \bar{k} \bar{l} \bar{o} \bar{p}$. This will create a number of unit clauses, including the assignment clause, and will immediately lead to a satisfying assignment:
$c m e g j n s \bar{k} \bar{q} \bar{d} \bar{r} \bar{a} \bar{b} \bar{i} \bar{l} \bar{o} \bar{p} \bar{h} \bar{r}$
$(C,k,q)(d,M,r)(a,b,C)(a,d,E)(f,G,h)(b,d,G)(i,J,k)(i,l,M)(N,o,p)(J,l,o)(h,p,S)(q,r,S)(k,N,r)$
What, if anything, is wrong with this proof?
For example, does anyone see a situation that would require this algorithm to backtrack other than processing a conflict cluster?
The algorithm could add $O(m^4)$ assignment clauses. Can this cause the algorithm to take more than a polynomial number of steps to process?
