Apply resolution algorithm to check SAT for CNF

659 Views Asked by At

I have a CNF:

$$(\neg p \lor \neg q \lor r) \land (\neg p \lor \neg r) \land p \land q$$

I need to check SAT for it using resolution algorithm, but i don't know how. I know how to check it with truth table, but not with resolution algorithm. I don't really see how to transform it further to find (or not find) a contradiction. How to apply resolution algorithm for this CNF and if its satisfiable find all satisfying assignments?

1

There are 1 best solutions below

0
On BEST ANSWER

To apply the resolution method, from you formula in conjunctive normal form (CNF) $$(\neg p \lor \neg q \lor r) \land (\neg p \lor \neg r) \land p \land q$$ you get the starting clauses $$ \neg p \lor \neg q \lor r \qquad \neg p \lor \neg r \qquad p \qquad q $$ If there is a way to derive the empty clause $\bot$ by applying the resolution method (i.e. by applying iteratively the resolution rule to the starting clauses and to the clauses you get after a resolution), then the CNF is unsatisfiable.

In this case, there is a way to derive $\bot$ by applying the resolution method, and hence the initial CNF is unsatisfiable. Indeed,

\begin{align} 1. \qquad &\neg p \lor \neg q \lor r &\text{given} \\ 2. \qquad &\neg p \lor \neg r &\text{given} \\ 3. \qquad &p &\text{given} \\ 4. \qquad &q &\text{given} \\ 5. \qquad &\lnot r &\text{resolution from 2. and 3.} \\ 6. \qquad &\lnot p \lor \lnot q &\text{resolution from 1. and 5.} \\ 7. \qquad &\lnot q &\text{resolution from 6. and 3.} \\ 8. \qquad &\bot &\text{resolution from 4. and 7.} \end{align}