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?
a+b
anda+!b+c
witha+c
, because there is no rule allowing this. $\endgroup$