Satisfiabililty sufficient condition?

Question

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).

Answer 1

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".