Apply resolution algorithm to check SAT for CNF 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?
 A: 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}
