DPLL

The DPLL algorithm (named after its inventors) comprises two main steps:

• Splitting
• Unit propagation

If any clauses contain only a single literal, its value can be immediately determined and does not need to be guessed. This means that, for example, if a set of clauses contains the clause $p$, we do not need to consider the case when $p=0$. Equally, if there is a clause $\neg q$, then we know that $q=0$, and in both cases we propagate these results to the other clauses using two rules: For a clause containing only a literal $A$:

• Delete all clauses containing $A$,
• Delete occurrences of $\neg A$ from all clauses.

Note

$A$ is required to be a literal, not an atom, so a clause $\neg p$ would require the deletion of clauses containing $\neg p$ and the deletion of occurrences of $p$ from all clauses.

These two rules constitute unit propagation.

If there are no clauses containing only a single literal, then a variable should be selected to split, and the two cases for this variable should be considered

If, at any point, any of the clauses becomes empty (denoted as $\square$), the set of clauses is unsatisfiable. This will occur when the only literal in a clause is deleted. If all clauses are deleted to obtain the empty set of clauses (denoted as $\{\}$), the set of clauses is satisfiable.

Warning

It is important to understand the distinction between the empty clause ($\square$) and the empty set of clauses ($\{\}$) and how these are obtained.

DPLL Optimisation §

Tautology elimination §

Any clause which takes the form $p\vee \neg p\vee C$ is tautological and can be deleted from the set of clauses without affecting satisfiability.

Pure literal elimination §

For every literal in the set of clauses, if its negation does not occur anywhere in the set of clauses, this literal is pure. Every clause containing a pure literal can be deleted.

Note

This rule may become applicable at some point during the execution of the algorithm, so it is important to re-check after each propagation.

Horn clauses §

A clause is horn if and only if it contains at most one positive literal. A set of horn clauses and a single-literal clause can always have its satisfiability ascertained through repeated unit propagation.