The Davis‑Putnam algorithm (DPLL)

A propositional formula is satisfiable if there is at least one assignment of its variables that makes it true (T). If it is false under every assignment, it is unsatisfiable.

Knowing whether a formula is satisfiable is a central problem in Computer Science, because many problems from other areas can be expressed in those terms: optimisation (planning, scheduling), combinatorics (graph colouring) and first-order theories (SMT solvers).

The most direct way to answer is to build the truth table and look for a row where the formula is T. With n variables the table has 2ⁿ rows: each extra variable doubles the work. And, in the worst case, nothing better is known: no algorithm for SAT is known that is not exponential in the number of variables and connectives of the formula (SAT is NP-complete).

But in the general case we can do much better than brute force. The idea is to build, little by little, a partial assignment that satisfies the formula, instead of generating complete assignments (truth table rows) and checking each one. That is what the Davis-Putnam algorithm does, and it is especially simple when the formula is in conjunctive normal form (CNF), written as a set of clauses: the topic of §2.

A literal is a variable (p) or the negation of a variable (¬p). A clause is a disjunction of literals l₁ ∨ l₂ ∨ … ∨ lₙ, with n ≥ 0, and can be represented by the set of its literals: p ∨ ¬q ∨ ¬p ∨ s is represented by {p, ¬q, ¬p, s}. Since it is a set, order does not matter and a repeated literal counts only once.

If n = 0, the clause is empty and corresponds to F: it has no literal that could make it true. If n = 1, the clause is unitary (for example, {¬p}).

Any formula in CNF can be represented by a set of clauses, read as the conjunction of those clauses. For example, ¬p ∧ (q ∨ r ∨ q) ∧ (¬r ∨ ¬s) ∧ (p ∨ s) ∧ (¬q ∨ ¬s) corresponds to the set {{¬p}, {q, r}, {¬r, ¬s}, {p, s}, {¬q, ¬s}}. It is also common to write each clause as a disjunction: {¬p, q ∨ r, ¬r ∨ ¬s, …}.

This gives the two cases where the algorithm stops. The empty set {} has no clause to satisfy, so it is satisfiable. A set that contains F has a clause that no assignment makes true, so it is unsatisfiable.

In the tool you can write a set in any of the three notations: the compact one from the exercises' «Input» lines (p1, -p1 -p2), set notation or logic notation. Try the converter: the same set shows up in all three.

Complementary literals: given a literal l, its complement l̃ is ¬l if l is a variable (positive literal) and p if l is of the form ¬p (negative literal). For example, the complement of p is ¬p and the complement of ¬p is p.

A clause is a tautology if it contains a pair of complementary literals p and ¬p, such as {p, ¬q, ¬p, s}. It is true under every assignment, so it can be removed from the set without changing satisfiability. Here tautologies are flagged but not removed: the tool's DLL treats them like any other clause.

A unit clause {l} has a single literal, so it is only true if l is true. There is nothing to choose: every valuation that satisfies S must make l true. Unit propagation uses this to simplify S without losing any solution.

Given a set of clauses S, a set S′ is obtained from S by unit propagation by repeating the following transformation: if S contains a unit clause l, then

1. remove from S all clauses of the form l ∨ C′ (they are true when l is true; {l} itself also goes);
2. replace in S each clause of the form l̃ ∨ C′ with the clause C′ (l̃ is false, so it no longer helps satisfy the clause).

In the diagram p is propagated: {p} and p ∨ q contain p and go away (rule 1); ¬p ∨ r loses ¬p and becomes r (rule 2); q ∨ s has neither p nor ¬p and stays the same.

Notice that rule 2 can create new unit clauses (¬p ∨ r became r), so the transformation is repeated while there are unit clauses. And if the clause {l̃} is also in S, it loses its only literal and becomes F, the empty clause: the set is unsatisfiable.

Try it with the set below: click a unit clause to propagate it and watch both rules at work. In this example F is reached using unit propagation alone.

In the DLL pseudocode this step is S := propagate(S). The tool propagates one literal at a time and always uses the first unit clause in the order of the set; here you can pick another one to see that the rules are the same. When propagation stops with S neither empty nor containing F, a literal has to be chosen to branch on: that is the topic of §4.

When unit propagation stops, S is in one of three cases: it is empty (every clause was satisfied, so S is satisfiable), it contains F (there is a clause no assignment satisfies, so S is unsatisfiable), or neither. In the third case there is nothing more to deduce and we have to try: pick a literal l and first try S ∪ {l}; if that branch is unsatisfiable, try S ∪ {l̃}. This is the DLL algorithm (Davis, Logemann and Loveland), in pseudocode:

Adding {l} to S adds a unit clause, so the recursive call DLL(S ∪ {l}) starts by propagating l. Since every assignment makes l or l̃ true, S is satisfiable if and only if S ∪ {l} or S ∪ {l̃} is: the two branches cover every case, and the algorithm only answers unsatisfiable when every branch reaches F.

The same algorithm as a flowchart, with a two-branch example, {¬p ∨ ¬q, ¬p ∨ q, p ∨ ¬q, p ∨ q}. This set has no unit clauses, so a literal has to be chosen right away. Step through it and see which box of the flowchart matches each step; the dashed arrows are the recursive calls, which go back to the start with the new set.

The tool always picks the first variable in alphabetical order with the positive branch first, so here it starts with p; starting with ¬p would be just as valid. In this example it makes no difference: in both branches propagation gives {¬q, q} and then {F}, and DLL(S) returns unsatisfiable. In §5 you will see when the choice of literal changes the size of the tree.

When propagation stops and S is neither empty nor contains F, DLL has to choose a literal: this is the l := select_literal(S) of the pseudocode. This function can be seen as a parameter of the algorithm, since an appropriate choice of literal can make it more efficient. The answer (satisfiable or unsatisfiable) is always the same; what changes is the path and the size of the tree. Possible criteria are to choose a variable that:

• occurs more often;
• has the maximum product of the occurrences of l and l̃;
• occurs most often in clauses of minimum size;
• etc.

Once the variable is chosen, the sign is left, that is, which of the two branches is tried first. You can start with p or with ¬p; the tool always uses the first variable in alphabetical order and the positive branch first. On an unsatisfiable set the sign does not change the size of the tree: DLL only answers unsatisfiable after both branches reach F, so only the order changes. On a satisfiable set, picking the right branch first saves the whole other branch.

Compare the two choices on the same set. Each node is a call DLL(S); the leaves end in ✓ (S empty) or ✗ (S contains F). Try the criteria above too: on the 8-variable set, with the positive branch first, alphabetical order gives 6 nodes and the variable that occurs most often in clauses of minimum size gives 3.

No sign is always best: in «Three variables B» the positive branch wins and in «Three variables E» the ¬ branch wins. That is why the criteria above look at the set instead of following a fixed order. The tool keeps alphabetical order with p first, a fixed rule that is easy to follow by hand, so you can compare your solution with the Step by step page. If you choose another literal the path changes, but the conclusion is the same.

The Davis-Putnam algorithm, from 1960, is an initial version that is still the basis of many of the most efficient algorithms today (like those in the SAT Competition). The basic idea is to consider the possible truth values of each variable and simplify the formula according to them until it is possible to conclude whether it is satisfiable or not.

That 1960 version, by Martin Davis and Hilary Putnam (the paper “A Computing Procedure for Quantification Theory”, in the Journal of the ACM), worked on a set of clauses with three rules: unit clause propagation (the one from §3), pure literal elimination (if the complement of l does not occur in S, l can be made true and the clauses with l are removed) and the elimination of a variable by resolution. There was no branching: the set kept being transformed until it was empty (satisfiable) or contained F (unsatisfiable).

Resolution combines two clauses with complementary literals: from p ∨ C and ¬p ∨ D you get the resolvent C ∨ D. Any valuation that satisfies both satisfies C ∨ D, because p or ¬p is false. To eliminate p, all clauses with p and with ¬p are replaced by all the resolvents of those pairs; the new set no longer has p and is satisfiable if and only if S is. Resolvents that are tautologies can be discarded. In the figure, the two-branch example from §4: eliminating p gives {¬q, q} (two of the four resolvents are tautologies) and propagating ¬q leaves F.

The problem is size. If p occurs in k clauses and ¬p in m, elimination replaces those k + m clauses with up to k · m resolvents, and each one can be longer than the clauses it came from. In many sets the number of clauses explodes and, on the computers of the time, memory was not enough.

In 1962, Martin Davis, George Logemann and Donald Loveland (“A Machine Program for Theorem-Proving”, in Communications of the ACM) replaced elimination by resolution with branching: choose a literal l and try S ∪ {l} and then S ∪ {l̃}, as in §4. Instead of keeping an ever larger set, a tree is explored depth-first and only the current path is kept. This algorithm, DLL (also called DPLL), is often also presented under the name Davis-Putnam, and it is the one this tool uses.

Eight questions to check what you have read: some are multiple choice and others ask «what is the next step?», where you play the part of DLL. After each answer you see the reason, with the rule that applies. Your best score is saved in this browser.