Using the DPLL Algorithm to show that φ is satisfyable

Question

I've got a WFF here that I need to prove is satisfiable through the DPLL algorithm. φ ≡ {{p1, ¬p2, p3, p4}, {¬p1, p2, ¬p3}, {¬p3, p4}, {¬p2, p3}, {p1, ¬p4}}

My understanding of DPLL is that I continually run the unit rule and the pure rule until φ has an empty clause. However, I can't use the unit rule because every clause has more than one literal, and I can't use the pure rule because every literal appears as a negative and positive.

I'm a bit stuck and I'd appreciate any help. I'm sorry if I said something dumb, I'm very new to logic.

Answer 1

You can indeed not solve this one using just the unit or the pure rule. However, there is also a splitting rule (indeed, one can argue that the splitting rule really lies at the heart of DPLL): Focus on one of the atomic variables, and consider the case where it is true, and the case where it is false, where you 'reduce' the clause set with regard to the truth of that atomic variable. If in both cases you reach the empty clause, then the clause set is unsatisfiable.

So, in your example, let's pick $p1$ as the atomic proposition to split on.

Now, when $p1$ is true, then that will automatically satisfy any clause that contains $p1$, so we can remove that one from the set of clauses to be satisfied. So, we can remove clauses 1 an 5. Also, any clause that contains $\neg p1$ will of course not be satisfied by our setting of $p1$ to true, so we might as well remove that $\neg p1$ from the clause. So, remove $\neg p1$ from clause 2. This leaves us with:

$$\{ \{ p2, \neg p3 \}, \{\neg p3, p4 \}, \{\neg p2, p3 \} \}$$

And now just repeat the loop: keep applying the unit or pure rule where possible (you can apply the pure rule), and if neither applies, split again, etc.

Now, to test your understanding, can you tell me what the result is of reducing the original clause set when we set $p1$ to false (or, in other words, when we reduce the set with regard to $\neg p1$?)

Also: can you tell me what it would mean if, when splitting on some variable, one branch leads to an empty clause, but the other branch does not?