1
$\begingroup$

I have the following set of clauses

$\{\{\neg A, \neg B, C\}, \{\neg E, B\} \{\neg A, \neg C, D\}, \{A\},\{B\},\{\neg D, \neg C, \neg B, E\}, \{\neg A, \neg E, \neg F\}\}$

I'm supposed to show that the set of clauses is satisfiable using resolution. I know that resolution only tells you if a set of clauses is unsatisfiable if you can derive the empty clause. But how do I show the satisfiability?

$\endgroup$
3
$\begingroup$

Given finite set of clauses, each of which contains only finite literals, there are only a finite number of possible clauses you can obtain through resolution. So, if the clause set is satisfiable, there will have to be a point at which no new clause can be resolved. At that point, you know that the original clause set is satisfiable.

As far as your specific clause set goes: there are $11$ different literals (there is no $\neg F$), so that would mean that there are $2^{11}=2048$ possible clauses that resolution could possibly come up with. As such, if you run the resolution algorithm on a decent computer, it should fairly quickly run out of new clauses to obtain. But, by hand, this number is probably a bit too large for comfort.

Fortunately, the actual number might be a good bit lower than that (for example, I see no way to obtain the clause that contains all of those $11$ literals), so you could just give it a go by hand. Thus, we could for example list all existing clauses, and then systematically see what new ones we can obtain. One way to do this systematically is simply to loop:

Find the first two clauses that can be resolved into a clause you don't already have (to find those 'first' two, you could e.g. set $i=1$ and $j=2$, see if clauses $i$ and $j$ can be resolved into a new clause; if not, increase $j$; and if $j$ runs out, increase $i$ by $1$ and set $j=i+1$ and repeat). Add the new clause to the list. Repeat .. until there is no new clause to resolve.

  1. $\{\neg A, \neg B, C\}$

  2. $ \{\neg E, B\}$

  3. $ \{\neg A, \neg C, D\}$

  4. $ \{A\}$

  5. $\{B\}$

  6. $\{\neg D, \neg C, \neg B, E\}$

  7. $ \{\neg A, \neg E, \neg F\}$

  8. $\{\neg A, \neg E, C\}$ 1,2

  9. $\{\neg A, \neg B, D\}$ 1,3

  10. $\{\neg B, C\}$ 1,4

  11. $\{\neg A, C\}$ 1,5

  12. $\{\neg A, \neg D, \neg B, E\}$ 1,6

  13. $\{\neg D, \neg C, \neg E, E\}$ 2,6

  14. $\{\neg A, \neg B, \neg D, \neg E, E\}$ 1,13

  15. $\{\neg D, \neg C, \neg B, B\}$ 2,6

etc.

Hmm, that still looks quite a few... Well, there are some other things you can do to speed this up:

  1. Tautologous clause elimination/prevention: Note how clause $13$ is tautologous: whether $E$ is set to true or false, clause $13$ will be satisfied. Hence, clause $13$ can effectively be removed from the clause set. Indeed, you can easily prove that for any clause set $C$: $C$ is satisfiable iff $C'$ is satisfiable, where $C'$ is clause set $C$ with all tautologous clauses removed. Indeed, we can update our algorithm to skip resolving two clauses that would result in a tautologous clause.

  2. Subsumed clause elimination/prevention: Note that if clause $5$ is satisfied, clause $2$ will automatically be satisfied as well. So, we can simply disregard clause $5$. Or, in general, we can remove any 'subsumed' clauses $C$, which are clauses for which there exists some other clause in the clause set that is a strict subset of $C$: again, we can easily prove that for any clause set $C$: $C$ is satisfiable iff $C'$ is satisfiable, where $C'$ is clause set $C$ with all subsumed clauses removed. And again, we can instruct the algorithm to never create a clause that's already subsumed by some other clause.

  3. Pure literal elimination: as pointed out, we have a $\neg F$ in clause $7$, but no $F$ anywhere else. This means that we are free to set $F$ to false in order to satisfy clause $7$, and doing this will yet again not effect the satisfiability of the rest of the clauses. So, we can just remove clause $7$.

  4. Unit clause preference: Given clause $5$, which is called a 'unit' clause, since it contains exactly one literal, we obviously need to set $B$ to true. This means that we can remove any $\neg B$ from any of the other clauses, since obviously those clauses are not going to be satisfied by the $\neg B$. In general, we can show that for any clause set $C$: $C$ is satisfiable iff $C'$ is satisfiable, where $C'$ is clause set $C$ with all unit clauses removed, and where the complements of the literals that were in those unit clauses have been remomed from all other clauses. Since unit clauses simplify things greatly, resolving with unit clauses should have preference, and again we can instruct our algorithm to do exactly that.

So, let's apply these simple techniques to your clause, and see if things are getting any better. First, remove subsumed clause $\{\neg E, B\}$:

$\{\{\neg A, \neg B, C\}, \{\neg A, \neg C, D\}, \{A\},\{B\},\{\neg D, \neg C, \neg B, E\}, \{\neg A, \neg E, \neg F\}\}$

Then, remove clause $\{\neg A, \neg E, \neg F\}\}$ due to its pure literal $\neg F$:

$\{\{\neg A, \neg B, C\}, \{\neg A, \neg C, D\}, \{A\},\{B\},\{\neg D, \neg C, \neg B, E\}\}$

And now $E$ has become a pure literal, so we can remove $\{\neg D, \neg C, \neg B, E\}$:

$\{\{\neg A, \neg B, C\}, \{\neg A, \neg C, D\}, \{A\},\{B\}\}$

And now $D$ has become pure:

$\{\{\neg A, \neg B, C\}, \{A\},\{B\}\}$

and now $C$:

$\{\{A\},\{B\}\}$

And both of them:

$\{\}$

And an empty clause set is trivially satisfiable ... meaning that the original set was satisfiable as well. And, if we look back on the process, we know exactly how to satisfy this clause set: set $F$ to false, and all others to true.

And, a funny thing just happened: we never actually did resolve any new clauses at all!

$\endgroup$
  • $\begingroup$ Is that the only way using resolution to tell if the clause is satisfiable? $\endgroup$ – Javiator May 8 '18 at 19:39
  • $\begingroup$ @Javiator you can do it efficiently ... still working on my Answer to show that ... $\endgroup$ – Bram28 May 8 '18 at 19:49
  • $\begingroup$ I wish I could upvote this answer 100 times. Thank you so much for this detailed answer. I really learned a lot! $\endgroup$ – Javiator May 8 '18 at 20:27
  • $\begingroup$ @Javiator You're welcome! It was a good refresher for me :) $\endgroup$ – Bram28 May 8 '18 at 20:29
  • $\begingroup$ I'm pretty sure they want you to just go in order...eliminate $A$, then eliminate $B$, then eliminate $C$ etc until $F$ is left, then depending on the terminating conditions maybe backtrack with the the resulting atomic disjuncts at the end of the alphabet to construct atoms for the start of the alphabet. $\endgroup$ – DanielV May 9 '18 at 22:56

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.