3
$\begingroup$

The conjecture itself:

k-SAT formula is satisfiable if no pair of unit assignment $l$ and $\overline l$ imply the formula to contain unsatisfiable (k-1)-SAT.

Example (XOR-SAT has no edges and cycles in implication graph, so it's simple example):

$$(\overline x\oplus y\oplus z)\land(x\oplus y\oplus v)\land(x\oplus y\oplus w)\land(x\oplus z\oplus v)\land(x\oplus z\oplus w)\land(x\oplus v\oplus w)$$

If in this formula we'll put $x$, we get $(y\oplus z)\land(y\oplus\overline v)\land(z\oplus\overline v)$ which is unsatisfiable.

So, we only can put $\overline x$: this yields us $(y\oplus v)\land(y\oplus w)\land(v\oplus w)$ which is also unsatisfiable.

Now we conclude that formula is unsatisfiable.

My thoughts on it:

The rule surely works if $k = 2$: 2-SAT is unsatisfiable iff there are two unit assignments $l$ and $\overline l$ that make the formula to contain unsatisfiable 1-SAT (two opposing unit clauses).

In fact algorithm would be:

for i = 1..n
    assign x_i
    while unit clauses are presented
        apply unit propagation
    if opposing unit clauses found
        assign -x_i
            while unit clauses are presented
                apply unit propagation
            if opposing unit clauses found
                return UNSAT
return SAT

And it does actually the same as implication graph analisys (primitive, though).

But what about $k > 2$?

For $k=3$ we'd need to change algorithm:

for i = 1..n
    assign x_i
    while unit clauses are presented
        apply unit propagation
    run algorithm for 2SAT
    if 2SAT returned UNSAT
        b_i = 1
    assign -x_i
    while unit clauses are presented
        apply unit propagation
    run algorithm for 2SAT
    if 2SAT returned UNSAT
        b_i += 2
    if b_i == 3
        return UNSAT
    else if b_i == 2
        add clause x_i
    else if b_i == 1
        add clause -x_i
    if b_i > 0
       i = 1
return SAT

Maybe this is not the best implementation, but this is the idea of algorithm. It applies unit assignment and then solves 2SAT for all 2-clauses, in fact it finds all connectivities between opposing literals (finding connectivity between $x$ and $\overline x$ means new unit clause).

$\endgroup$
  • 2
    $\begingroup$ Have you tried writing a program to enumerate all formulas on 3 variables to see if your conjecture holds for them? on 4 variables? That would be a good starting point. Or, generate millions of random formulas and see if your conjecture holds for all of them. $\endgroup$ – D.W. Jul 12 '17 at 0:30
  • 1
    $\begingroup$ Here's another thing I'm not clear on. Suppose we have three clauses $f,g,h$. In step 2 we modify $f$ based on $g$. Then we modify $f$ based on $h$. In step 3 are we analyzing the modified $f$ that includes both modifications? Or is step 3 done separately for each pair of clauses, with modifications from only the other clause? $\endgroup$ – D.W. Jul 12 '17 at 21:33
  • 1
    $\begingroup$ @D.W. Thanks, it represents what I'm asking. In step 2 each modification is permanent. So, when we modify $f$ based on $h$, we have $f$ that is already modified by $g$. So, in step 3 $f$ includes both modifications. Step 3 doesn't check pairs, it works with single truthtables. $\endgroup$ – rus9384 Jul 12 '17 at 21:41
  • $\begingroup$ @rus9384 Do you already know the answer to your open question: "Satisfiability sufficient condition?"? Did you find another counterexample to your new updated conjecture or does your conjecture really imply that $P=NP$ at last? If you still don't know and your question is still open and unknown then I suggest or recommend you to start bounty for your question and if the answer to your question will prove that $P=NP$ then the reward you will get and receive for that will be much greater than the number of reputations that you will spend for the bounty. $\endgroup$ – Farewell Stack Exchange Aug 12 '17 at 20:29
  • $\begingroup$ @rus9384 I am voting to close this question as off topic, because it is an attempted proof that $P=NP$. Don't worry I am just joking only :D I have already liked, upvoted and favorited your question. $\endgroup$ – Farewell Stack Exchange Aug 18 '17 at 14:54
-1
+50
$\begingroup$

taking the contrapositive, another stronger way of stating your question is "a SAT formula f is satisfiable iff either the sub-formulas f1, f2 from the assignment of a variable x or not x are satisfiable". but this is exactly the idea behind the DPLL algorithm (originating as the simpler DP algorithm) provably guaranteed to find a SAT solution. your basic idea also shows the similarity of the method with Gaussian reduction; ie this is not usually remarked but DPLL algorithm appears to be like/ an analog of "boolean Gaussian reduction".

$\endgroup$
  • 1
    $\begingroup$ DPLL applies this idea recursively. The OP's algorithm doesn't. $\endgroup$ – Yuval Filmus Aug 20 '17 at 15:09
  • 1
    $\begingroup$ ah, ok. his "conjecture" stated at top is different than his algorithm. the algorithm uses unit propagation. the answer applies to the conjecture. re the algorithm, it is not possible to determine satisfiability of formulas in general with mere unit propagation, there are many counterexamples. $\endgroup$ – vzn Aug 20 '17 at 15:54
  • 1
    $\begingroup$ My algorithm, as well as conjecture, asks if there are unsatisfiable 3CNF formulas in which no unit assignment will turn a formula to one containing unsatisfiable 2CNF. In fact I asked for counterexample. $\endgroup$ – rus9384 Aug 20 '17 at 21:10
  • 1
    $\begingroup$ the conjecture talks only about "unit assignment" (which my answer focused on) and the later stuff talks about "unit propagation". sorry, find it hard to follow, dont think its consistent. maybe you want to define "unit assignment". seems like there may be multiple questions going on here. could try to disentangle them in Computer Science Chat if you want. $\endgroup$ – vzn Aug 21 '17 at 2:04

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.