0
$\begingroup$

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$
4
  • $\begingroup$ What is exactly your process in the first example - do you want to replace both Clause1 and Clause2 with Resolution (you can't to that on step 2, for example)? What is the final set of clauses you get? $\endgroup$
    – mihaild
    Commented Dec 30, 2021 at 19:06
  • $\begingroup$ In the first example, I was replacing Clause 1 & Clause 2 with the resolution (Clause R1). I then replaced R1 & Clause 3 with R2... and so on, so the end result is a single resolution (!a + !c). I get that this is resulting in the wrong answer - but I can't figure out what rule I'm breaking with this method. $\endgroup$ Commented Dec 30, 2021 at 19:16
  • $\begingroup$ In the second step, you can't replace a+b and a+!b+c with a+c, because there is no rule allowing this. $\endgroup$
    – mihaild
    Commented Dec 30, 2021 at 19:20
  • $\begingroup$ I see the error now - thank you for pointing it out. I will accept the original answer as it answered everything required to understand the problem. The 2nd step (and further) was my lack of thinking. $\endgroup$ Commented Dec 30, 2021 at 19:43

2 Answers 2

0
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ milhaid, thanks for the reply. The last section makes sense - up to a point. In my first example, where I continuously re-used the resolution, it appears that I'm following all these rules. In each case, the resolution is a subset of at least 1 original clause and if it's satisfied, so is the original clause. I'm still missing something - I'm not following when the original clause can be removed. $\endgroup$ Commented Dec 30, 2021 at 18:51
0
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .