1
$\begingroup$

Exercise: Transform the set of formulas $\{p, p→((q ∨r)∧¬ (q ∧r)), p→((s ∨t)∧¬ (s ∧t )), s→q, ¬r→t, t→s \}$ into clausal form and refute using resolution.

Solution:

Clausal form: $S=\{(1)p,\overline pqr,\overline p\, \overline q\,\overline r,\overline sq,rt,\overline ts,\overline pst,(8)\overline p\,\overline s\,\overline t\}$

Using resolution:

(9) $q\overline t\ $ 4,6

(10) $\overline p\, \overline t\,\overline r\ $ 3,9

(11)$\overline r\overline t\ $ 1,10

(12)$\overline pq\overline t\ $ 11,2

(13)$\overline pqr\ $ 12,5

(14) ?

I'm stuck here since the only available clausal are (7) and (8) but none can be used with (13) i.e. the $\fbox {}$ cannot be derived by (13) with (7) or (8).

What do I do to solve this problem?

Any help for solving this problem is really appreciated.


This is the algorithm

Algorithm 4.18 (Resolution procedure) Input: A set of clauses S. Output: S is satisfiable or unsatisfiable. Let S be a set of clauses and define $S_0 = S.$ Repeat the following steps to obtain $S_{i+1}$ from $S_i$ until the procedure terminates as defined below:

• Choose a pair of clashing clauses ${C1,C2} ⊆ S_i$ that has not been chosen before.

• Compute C = Res(C1,C2) according to the resolution rule.

• If C is not a trivial clause, let $S_{i+1} = S_i ∪ {C};$ otherwise, $S_{i+1} = S_i $.

Terminate the procedure if:

• $C =\fbox{} $

• All pairs of clashing clauses have be resolved.

$\endgroup$

2 Answers 2

2
$\begingroup$

You are stuck because you are under the impression that you can use any clause just once, but that is not true: you can use any clause any number of times.

Also, here is a useful strategy: always try to use clauses that have a single literal if you can. So, for example, since you have clause $p$, resolve that with any of the clauses that have $p'$

$\endgroup$
4
  • $\begingroup$ You say I can use any clause any number of times, so what is the meaning of the first bullet in the algorithm? $\endgroup$ Mar 30, 2018 at 17:34
  • $\begingroup$ @Michelle It is a pair that has not been chosen before. Which makes sense, since if you resolve on a pair you've used before, you get the same result as before. But, reusing one clause, but combing it with a different clause gives you a new pair, and hence possibly a new resolvent clause. For example, combining $1$ and $2$ gives you $qr$, while combining $1$ and $3$ gives you $q'r'$, and that's new. Indeed, the pair 1 and 3 is not the same pair as 1 and 2 $\endgroup$
    – Bram28
    Mar 30, 2018 at 17:35
  • $\begingroup$ oh you're right I misunderstood pair with clause. Thanks for the strategy bwt :) $\endgroup$ Mar 30, 2018 at 17:48
  • 1
    $\begingroup$ @Michelle You're welcome! :) The strategy is called 'unit literal reduction', since with a singleton/'unit' clause, all clauses that contain the complement of that literal will get reduced in size .. which is why it is such a useful strategy! $\endgroup$
    – Bram28
    Mar 30, 2018 at 17:51
1
$\begingroup$

Tip: Pick literals in strategic order, or alphabetic, then consecutively resolve all pairs of clauses with conflicts in that literal, until no more unresolved conflicts in that literal remain (or you encounter an empty clause).   Then repeat for the remaining literals.   Thus ensuring that if you don't terminate you will have resolved all conflicting pairs, as the algorithm directs.

Note:

$\{p, p→((q ∨r)∧¬ (q ∧r)), p→((s ∨t)∧¬ (s ∧t )), s→q, ¬r→t, t→s \}$ into clausal form and refute using resolution.

$\{p, (\overline p, q , r), (\overline p, \overline q , \overline r), (\overline p,s,t), (\overline p,\overline s,\overline t), (\overline s,q), (r,t), (\overline t, s) \}$

Clearly the first move is to resolve away all pairs of $p$ vs $\overline p$ conflicts.

Notice: $\{p, (\overline p, q , r)\}, \{p, (\overline p, \overline q , \overline r)\}, \{p, (\overline p,s,t)\}, \{p, (\overline p,\overline s,\overline t)\}$ are all distinct pairs despite containing the same literal.

$\{(q , r), (\overline q , \overline r), (s,t), (\overline s,\overline t), (\overline s,q), (r,t), (\overline t, s) \}$

Alphabetise

$\{(q, r), (q,\overline s),(\overline q,\overline r),(r,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve away all the $q$ vs $\overline q$ conflicts

$\{(\overline r,\overline s),(r,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve away all the $r$ vs $\overline r$

$\{(\overline s,t),(s,t),(s,\overline t),(\overline s,\overline t)\}$

Resolve those $s$

$\{(t),(\overline t)\}$

Which is more clearly a contradiction, but resolve to an empty clause anyway.

$\{()\}$

$\endgroup$
2
  • $\begingroup$ In this exercise you used alphabetic order, How would it be with strategic order? $\endgroup$ Mar 30, 2018 at 17:54
  • $\begingroup$ Strategy would simply be picking the easiest to eliminate ($p$ was) or if possible a literal which seems likely to produce a contradiction. $\endgroup$ Mar 30, 2018 at 19:23

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.