10
$\begingroup$

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.

$\endgroup$
4
  • 6
    $\begingroup$ Have you tried implementing your algorithm and seeing how well it works on known-hard cases (such as those derived from factoring a 2048-bit integer, or breaking AES, or inverting SHA256)? $\endgroup$
    – D.W.
    Mar 31, 2020 at 0:03
  • $\begingroup$ Learned clauses force backtracking when the algorithm restarts. Learned clauses are never deleted. $\endgroup$ Mar 31, 2020 at 0:35
  • 1
    $\begingroup$ There are lower bounds against DPLL, that is, there are formulas for which provably DPLL takes exponential time, no matter how you implement it. $\endgroup$ Mar 31, 2020 at 7:28
  • $\begingroup$ The proofs for DPLL use the fact DPLL is equivalent to resolution. While I think I can show the learned clauses in this algorithm can be generated using resolution, this algorithm does NOT use resolution to generate the learned clauses. Proofs based on resolution wouldn't apply to the running time of this algorithm. $\endgroup$ Mar 31, 2020 at 21:24

2 Answers 2

17
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ I'm not seeing the issue here. Just because the problem is no longer an X3SAT problem doesn't mean it doesn't solve the initial problem. Leave the learned clauses as described. We don't need the learned clauses to have exactly one false literal (the learned clauses always are all false). There's only one step in the process which sets a literal to true, so there's no chance of accidentally having a learned clause be all true or having one of the original clauses have two true literals. $\endgroup$ Mar 31, 2020 at 13:43
  • $\begingroup$ I can solve the X3SAT and 3SAT components simultaneously. I deliberately don't propagate positive unit clauses because it makes the proof simpler. The CDCL procedure can be modified to handle any type of conflict and still generate a learned clause with 3 or less literals. $\endgroup$ Mar 31, 2020 at 21:22
  • 3
    $\begingroup$ @RussellEasterly Your proof as written doesn't address the point I made. Also, I encourage you to code up your algorithm and feed it some hard SAT instances to see empirically if it terminates in time polynomial to the size of the formula. If P=NP your algorithm should outperform every modern SAT solver so handily that there would be no doubt. If it doesn't perform that well, then it's a sure sign that you need to go back to the drawing board. $\endgroup$
    – Kyle Jones
    Apr 1, 2020 at 21:58
  • $\begingroup$ @KyleJones Why do you think I need to convert the learned clauses to X3SAT? You don't give any reason why I need to do that. If you insist that only one type of problem can be solved at a time, it would be simpler to convert the X3SAT instance to 2+SAT using the transformation I describe. The algorithm wouldn't change much solving a 2+SAT instance. Even in the 2+SAT version all.the learned clauses would only contain negated literals. $\endgroup$ Apr 1, 2020 at 23:49
  • 3
    $\begingroup$ @RussellEasterly You are displaying a very defensive posture, looking for reasons to dismiss the answers. You got answers from experts, and I hope you will keep an open mind and actually think what they are saying. Think for a while. $\endgroup$ Jun 2 at 20:25
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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