1
$\begingroup$

Trying to understand 3-SAT self-subsuming process

I've been studying solver theory and am trying to understand some of the basic concepts that I've been reading. In particular, the idea of self-subsuming (if I have the correct terminology here) is confusing me. It appears that it's possible to come to different conclusions based upon the order of processing - but I'm pretty sure that this possibility is wrong, so I'm trying to understand what I'm doing wrong and where my thinking is incorrect.

To make it simple, if we start with the following 8 clauses, we know that it's UNSAT

a + b + c
a + b + !c 
a + !b + c 
a + !b + !c
!a + !b + c
!a + b + c
!a + b + !c
!a + !b + !c

But, if I use self-subsuming logic, it appears to be SAT based on the following:

Clause 1, Clause 2 (resolve on) = Resolution

a + b + c,  a + b + !c   (c) = a + b  [Use resolution for next step of process]                     
a + b,      a + !b + c   (b) = a + c                    
a + c,      a + !b + !c  (c) = a + !b               
a + !b,     !a + !b + c  (a) = !b + c           
!b + c,     !a + b + c   (b) = !a + c       
!a + c,     !a + b + !c  (c) = !a + b   
!a + b,     !a + !b + !c (b) = !a + !c

But, using a different process, it does become UNSAT. Here, the resolutions are kept separate until all 8 clauses have been reduced.

a + b + c,   a + b + !c   (c) = a + b
a + !b + c,  a + !b + !c  (c) = a + !b
!a + !b + c, !a + b + c   (b) = !a + c
!a + b + !c, !a + !b + !c (b) = !a + !c

Finally, use the 4 remaining clauses and you end with a contradiction - which we know is the correct answer.

a + b,       a + !b       (b) = a
!a + c,      !a + !c      (c) = !a

However, using the same remaining 4 clauses, processed differently it again appears SAT

a + b, !a + c   (a) = b + c 
a + !b, !a + !c (a) = !b + !c

Can someone explain what I'm doing wrong to come to different conclusions?

$\endgroup$
1
$\begingroup$

In the Resolution proof system, at any given point in time, we have a set $S$ of clauses. If $S$ contains two clauses $\alpha \lor x$ and $\beta \lor \lnot x$, we can resolve to obtain the new clause $\alpha \lor \beta$, which we add to $S$. We do not remove the original clauses. Rather, they stay in $S$.

A given collection of clauses is either satisfiable or unsatisfiable — this is a concept that has nothing to do with Resolution: a set of clauses is satisfiable if there is a truth assignment that satisfies all clauses; otherwise, it is unsatisfiable.

Resolution is sound: starting with a set $S$ of clauses, any clause $\alpha$ which is produced by Resolution is logically implied by $S$, in the sense that any truth assignment satisfying $S$ also satisfies $\alpha$. In particular, if $S$ is satisfiable, Resolution would not derive the empty clause.

Conversely, Resolution is complete: if a set $S$ of clauses is unsatisfiable, then using Resolution, you can derive from it the empty clause, thus proving that $S$ is unsatisfiable. The proof could be rather long — there are many explicit examples which require exponentially long proofs, though in practice, in many cases much shorter proofs work.

One way to deduce the empty clause given an unsatisfiable $S$ is to repeat the following algorithm: while there exist two resolvable clauses in $S$ whose resolvent is not in $S$, resolve the two clauses and add the resolvent to $S$. This process must work. Furthermore, any Resolution proof can be framed as a particular instantiation of this algorithm; the culprit is that at any given point in time, there could be many different pairs of clauses which could be resolved, and finding the optimal pair is hard.

Finally, a bit about clause learning. Above I wrote that when we resolve two clauses, we do not remove them from the set of clauses. But in fact, early SAT solvers did erase the resolved clauses, unless they were axioms. The corresponding proof system, treelike Resolution, is known to be exponentially weaker than general Resolution; that is, there are instances which have short refutations (proofs of the empty clause) in general Resolution, but only long ones in treelike Resolution. Modern SAT solvers use a technique known as clause learning which allows them to harness the power of general Resolution.

$\endgroup$
2
  • $\begingroup$ Yuval, thanks for the detailed response. I was confused on the resolution process. I was interpreting the process as one where I could eliminate the original clauses after each resolution step. It appears this is possible to remove the original clauses but on IFF every instance of x is resolved with every instance of ¬x. $\endgroup$ Dec 30 '21 at 20:46
  • 1
    $\begingroup$ Right, you can eliminate a variable in this fashion, and then you have no use for clauses involving this variable. If you do this repeatedly, you get what is known as a truth table proof, which is probably the easiest way of showing that (even treelike) Resolution is complete. $\endgroup$ Dec 30 '21 at 20:49

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.