Trying to understand 3-SAT self-subsuming process

Question

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?

Answer 1

We can't remove clauses we used for resolution by default. Resolution just gives as new clause, and if it's sub-clause of some existing clause, we can remove the old (because if new clause is satisfied, so is the old one). We also can remove old clauses if they were the only one containing variable we resoluted by, because if new clause is satisfied, one of them is satisfied too, and we can satisfy the other by assigning this variable.

For example, in your last part, we can add b + c, but we can't remove a + b or !a + c, because neither of them is superset of b + c, and there are other clauses that include a.

Answer 2

It appears that based on the simple example set, a lot of coincidental results were originally obtained.

To add an example that elaborates on the accepted answer, it takes a little more work to eliminate the original clauses. As milhaid suggested, I should have resolved across all instances of a variable before eliminating the original clause.

For this example, selecting (a) to resolve on, each clause that contains 'a' must be paired with each clause that contains '!a'

Any resolution that contains a tautology is left blank.

a + b + c,  !a + !b + c 
a + b + c,  !a + b + c  = b + c
a + b + c,  !a + b + !c 
a + b + c,  !a + !b + !c    
        
a + b + !c, !a + !b + c 
a + b + !c, !a + b + c  
a + b + !c, !a + b + !c = b + !c
a + b + !c, !a + !b + !c    
        
a + !b + c, !a + !b + c = !b + c
a + !b + c, !a + b + c  
a + !b + c, !a + b + !c 
a + !b + c, !a + !b + !c    
        
a + !b + !c,    !a + !b + c 
a + !b + !c,    !a + b + c  
a + !b + !c,    !a + b + !c 
a + !b + !c,    !a + !b + !c    = !b + !c

It follows that the proper way to continue is by selecting another variable to resolve on. I will select (b), and pair each clause with a 'b' with each clause that contains '!b'

b + c, !b + c = c
b + c, !b + !c

b + !c, !b + c
b + !c, !b + !c = !c

This sequence properly results in an answer of UNSAT.