How does DPLL Algorithm Work? A Brief Explanation of DPLL

DPLL algorithm is widely used in artificial intelligence. To understand and work better on the theoretical side of artificial intelligence and decision science, we should understand the DPLL algorithm.

In this post, I will try to explain the DPLL as briefly and clearly as I can.

What is it used for?

DPLL algorithm is mostly used to understand if a logical proposition is unsatisfiable or not. DPLL algorithm makes our calculations a lot faster, with helping us reduce the total number of cases we need to check.

With DPLL algorithm, we try to check the most likely model for the proposition via setting some propositions true or false. If we see that, the proposition is still not possible to satisfy even in that case; we conclude that this proposition is unsatisfiable.

Figure 1: An example of logical proposition. How would you check whether it is unsatisfiable?

How does it work?

Our proposition should be in “Conjunctive Normal Form”

Before starting, we need to make sure that the proposition we have in hand is in Conjunctive Normal Form (fancy name :)).

It actually means a proposition filled with ∧ and ∨. So, basically you shouldn’t have any arrows. Your sub-clauses that are separated by parenthesis, should be separated by ∧ , not ∨. To achieve this, you should apply the following steps:

1. Replace (a ⇔ b) with (a ⇒ b) ∧ (b ⇒ a)
2. Replace (a ⇒ b) with (~a ∨ b)
3. Move negations inside e.g. :
   a) ~(~a) = a
   b) ~(a ∧ b) = ~a ∨ ~b
   c) ~(a ∨ b) = ~a ∧ ~b
4. Distribute ∨ over ∧:
   a ∨ (b ∧ c) = (a ∨ b) ∧ (b ∨ c)

Here you can see Figure 2 and Figure 3 are not in Conjunctive Normal Form. However, Figure 1 was in Conjunctive Normal Form.

Figure 2: Not in Conjunctive Normal Form, there is an arrow

Figure 3: Not in Conjunctive Normal Form, sub-clauses are separated by ∨, instead of ∧. 4th step should be applied.

DPLL Algorithm Methods to Apply

Unit-clause Heuristic

This basically means that if there is any letter standing alone in your Conjunctive Normal form, you should set it to true. Let’s see it again on Figure1.

~A is a unit-clause standing by itself.

For this proposition to be true, every sub-clause separated by ∧ should be true. Since ~A is standing alone, it should set true by setting A as false.

• Here we should set A = false.

Pure Symbol Heuristic

The letter that occurs only in the positive or negative format through the whole proposition. In figure 4, we see that A and B both occurs in positive and negative forms ( A, ~A, B, ~B). However C is only in positive form.

In these cases if pure symbol always occurs positive, it should be set true; if it always occurs negative, it should be set false.

Figure 4: C is a pure symbol.

• Here we would need to set C = true.

Early Termination

If all sub-clauses that separated by ∧ are true; then the proposition is satisfiable. If all sub-clauses are false, then the proposition is unsatisfiable.

OK, but how to proceed?

Step 1: You should check if any of these DPLL methods are applicable for your proposition at the moment. If yes, apply it and come again to Step1 with the new proposition created after the last step.

Step 2: If there was no DPLL method applicable, randomly set a letter true, and continue with that. After finishing this branch if we find that this proposition is satisfiable, then we conclude that it is satisfiable. If it was unsatisfiable, we will come back here and set this variable false this time to check

Thank you for reading!!!