# Satisfiabililty sufficient condition?

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
else if b_i == 1
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).

• 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.
– D.W.
Jul 12, 2017 at 0:30
• 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?
– D.W.
Jul 12, 2017 at 21:33
• @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. Jul 12, 2017 at 21:41
• @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. Aug 12, 2017 at 20:29
• @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. Aug 18, 2017 at 14:54