Davis–Putnam–Logemann–Loveland Algorithm

propositional-logic sat-solving

Definition

Davis–Putnam–Logemann–Loveland Algorithm

The DPLL algorithm is a recursive decision procedure for the satisfiability of a set of clauses.

It is a refinement of the splitting algorithm that adds unit propagation at each recursive step before choosing a literal to branch on.

Procedure

Bool DPLL(Set Clause S)
    S = unit_propagate(S);
    if (S is empty) {
        return satisfiable;
    }
    if (□ ∈ S) {
        return unsatisfiable;
    }
    L = select_literal(S);
    if (DPLL(S ∪ {L}) == satisfiable) {
        return satisfiable;
    }
    return DPLL(S ∪ {¬L});

Explanation

Steps

1. Propagate. Apply unit propagation to simplify $S$ as far as possible.
2. Base cases.
   • If $S$ becomes empty, every clause was satisfied: return satisfiable.
   • If the empty clause $\square$ appears, a contradiction was found: return unsatisfiable.
3. Split. Choose an unassigned literal $L$ and try both branches recursively:
   • first assume $L$ is true (add the unit clause $L$);
   • if that fails, assume $L$ is false (add the unit clause $\neg L$).

The choice of $L$ is determined by the select_literal heuristic. Common heuristics include choosing a literal that appears most frequently, or one that occurs in the shortest clause.

Optimisations

Tautology Removal

Any clause $p\vee \neg p\vee C$ is a tautology. Tautologies can be removed.

Pure Literal Removal

Definition

Pure Atom Property

All clauses containing a pure literal can be satisfied by assigning a suitable truth value to the variable of this literal.

Link to original

Hence, clauses containing pure literals can be removed too.

Examples

Unsatisfiable set of clauses

Consider the set of clauses

$$S=\{\neg p\vee \neg q,\neg p\vee q,p\vee \neg q,p\vee q\}.$$

There are no unit clauses, so DPLL must branch. Choose literal $p$.

Left branch — assume $\neg p$.
Adding the unit clause $\neg p$ and applying unit propagation:

• $\neg p\vee \neg q$ and $\neg p\vee q$ are satisfied and removed;
• $p\vee \neg q$ simplifies to $\neg q$;
• $p\vee q$ simplifies to $q$.

The set becomes $\{\neg q,q\}$. Now $q$ is a unit clause, so propagation with $q$ removes $q$ and replaces $\neg q$ by the empty clause $\square$. Hence the left branch is unsatisfiable.

Right branch — assume $p$.
Adding the unit clause $p$ and applying unit propagation:

• $p\vee \neg q$ and $p\vee q$ are satisfied and removed;
• $\neg p\vee \neg q$ simplifies to $\neg q$;
• $\neg p\vee q$ simplifies to $q$.

The set becomes $\{\neg q,q\}$. As in the left branch, propagation yields the empty clause $\square$. Hence the right branch is also unsatisfiable.

Since both branches end in the empty clause, the original set $S$ is unsatisfiable.

Satisfiable set of clauses

Consider the set of clauses

$$S=\{\neg p\vee \neg q,\neg p\vee q,p\vee \neg q\}.$$

There are no unit clauses, so DPLL branches on literal $p$.

Left branch — assume $p$.
Adding the unit clause $p$ and applying unit propagation:

• $\neg p\vee \neg q$ simplifies to $\neg q$;
• $\neg p\vee q$ simplifies to $q$;
• $p\vee \neg q$ is satisfied and removed.

The set becomes $\{\neg q,q\}$. Propagation with $q$ removes $q$ and replaces $\neg q$ by the empty clause $\square$. The left branch is unsatisfiable.

Right branch — assume $\neg p$.
Adding the unit clause $\neg p$ and applying unit propagation:

• $\neg p\vee \neg q$ and $\neg p\vee q$ are satisfied and removed;
• $p\vee \neg q$ simplifies to $\neg q$.

The set becomes $\{\neg q\}$. Propagation with $\neg q$ empties the set. The right branch is satisfiable.

The model is obtained from the successful branch: we selected $\neg p$ and unit propagation derived $\neg q$. Hence

$$\{p\mapsto 0,q\mapsto 0\}$$

satisfies the original set $S$.