Davis–Putnam Algorithm

Decide clausal satisfiability by eliminating variables with resolution while preserving whether the clause set has a model.

Version

v3 · 2026-09-19 · History

Domain-specific #

1627

Domain group

Applied Sciences & Engineering

Origin domain

Computer Science & Software Engineering

Subdomains

Automated Theorem Proving, Propositional Satisfiability → Computer Science & Software Engineering

Aliases

DP procedure

Core Idea

The Davis–Putnam algorithm is a complete decision procedure for the satisfiability of a finite propositional formula in conjunctive normal form. It repeatedly simplifies a clause set and eliminates a selected propositional variable by resolution. If \(x\) occurs positively in clauses \(x\lor A_i\) and negatively in clauses \(\neg x\lor B_j\), the elimination step removes every clause containing \(x\) or \(\neg x\) and adds every non-tautological resolvent \(A_i\lor B_j\). The resulting formula may have different models and no longer mentions \(x\), but it is satisfiable exactly when the original formula is satisfiable.

How would you explain it like I'm…

Crossing Out Puzzle Questions

Imagine a puzzle with lots of rules about yes-or-no questions, like "either the light is on or the door is shut." You pick one question, combine the rules about it into new rules that don't mention it anymore, and throw the old ones away. You keep doing this. If you end up with a rule that can never be kept, the puzzle has no answer; if all the rules disappear, it has one.

Erase-a-Variable Rule Solver

The Davis–Putnam algorithm is a step-by-step method that decides whether a set of true-or-false rules can all be satisfied at the same time. The rules are written as lists of options where at least one must be true. The algorithm picks one variable and combines every rule where it appears as "yes" with every rule where it appears as "no," making new rules that no longer mention that variable. The new rules can all be satisfied exactly when the old ones could. It repeats this, also using some quick simplifying shortcuts. If it ever gets an empty rule that nothing can satisfy, the answer is no; if no rules are left, the answer is yes.

Satisfiability by Variable Elimination

The Davis–Putnam algorithm is a complete method for deciding whether a propositional formula in conjunctive normal form, an AND of OR-clauses, is satisfiable. Its key step eliminates one variable x by resolution: every clause containing x is combined with every clause containing not-x, producing new clauses that merge their other parts, skipping ones that are automatically true; then all clauses mentioning x are removed. The new formula has no x and may have different solutions, but it is satisfiable exactly when the original is. Simplifications such as the unit-clause and pure-literal rules can be applied along the way. The process ends when an empty clause appears, proving no solution exists, or when no clauses remain, proving one does. It is different from the later DPLL algorithm, which replaces this elimination with guessing a value and backtracking.

 

The Davis–Putnam algorithm is a complete decision procedure for satisfiability of a finite propositional formula in conjunctive normal form. Its core operation is variable elimination by resolution: if x occurs positively in clauses x ∨ A_i and negatively in clauses ¬x ∨ B_j, the step removes every clause containing x or ¬x and adds every non-tautological resolvent A_i ∨ B_j. The resulting formula no longer mentions x and may have different models, but it is satisfiable exactly when the original is; this equisatisfiability invariant is the algorithm's structural center. In effect, each elimination computes the constraints that remain after existentially projecting one Boolean variable away, which is a specific eliminative use of resolution rather than resolving until nothing new appears. Pure-literal and unit-clause rules may simplify the clause set before or between eliminations. The process terminates when an empty clause appears, certifying unsatisfiability, or when no clauses remain, certifying satisfiability. Davis and Putnam introduced it within a proof method for quantification theory, and its propositional stage became a foundational SAT procedure. It must be distinguished from the later Davis–Putnam–Logemann–Loveland (DPLL) procedure, which replaces the potentially explosive resolution-based elimination with case splitting and backtracking while retaining unit propagation.

Scope of Application

The direct scope is finite propositional CNF satisfiability. A formula in another propositional syntax may first be converted or encoded into CNF. When an encoding introduces fresh variables, equisatisfiability rather than literal equivalence is often the appropriate obligation. In the original quantification-theory setting, formulas were transformed through logical preprocessing until the propositional clause procedure could be applied.

The algorithm remains important in automated-reasoning history, SAT preprocessing, proof complexity, and variable-elimination methods. Bounded variable elimination in contemporary solvers uses the same resolution projection selectively, accepting an elimination only when growth is controlled.

Clarity

Treating a CNF formula as a clause set clarifies the two terminal objects. The empty clause \(\square\) is false under every assignment, so any clause set containing it is unsatisfiable. The empty set of clauses is an empty conjunction, hence true under every assignment, so it is satisfiable. Confusing these two “empty” cases reverses the algorithm's answer.

Manages Complexity

Variable elimination reduces the number of propositional variables and can expose unit clauses, pure literals, subsumption, and redundancy. A good elimination order can collapse structured instances rapidly. The method therefore transforms a global assignment problem into a sequence of local projections.

Its cost is the resolution cross-product. If \(x\) occurs in \(p\) positive and \(q\) negative clauses, eliminating it can generate as many as \(pq\) candidate resolvents before tautology and subsumption deletion.

Abstract Reasoning

Let \(F=R\land\bigwedge_i(x\lor A_i)\land\bigwedge_j(\neg x\lor B_j)\), where \(R\) contains no occurrence of \(x\). The eliminated formula is

\[ F'=R\land\bigwedge_{i,j}(A_i\lor B_j), \]

after tautological resolvents are discarded. If \(F\) has a model, every resolvent is true, so its restriction satisfies \(F'\). Conversely, suppose an assignment to the remaining variables satisfies \(F'\).

Knowledge Transfer

The transferable pattern is eliminate a local variable while deriving every constraint required to preserve global feasibility. Closely related patterns appear in database projection, probabilistic variable elimination, constraint satisfaction, and symbolic quantifier elimination. Transfer must respect the algebra of combination: Boolean resolution is not automatically valid in another substrate.

Within logic, the equisatisfiability discipline transfers directly to Tseitin encoding, Skolemization under appropriate satisfiability semantics, SAT preprocessing, and solver proof logging.

Relationships to Other Abstractions

Current abstraction Davis–Putnam Algorithm Domain-specific

Parents (1) — outgoing typed relations

• Davis–Putnam Algorithm is a kind of Algorithm Prime

  prime:algorithm is the broader abstraction this entry instantiates.

Hierarchy path (1) — routes to 1 parentless root

• Davis–Putnam Algorithm → is a kind of Algorithm → presupposes, conditional Function (Mapping)

Neighborhood in Abstraction Space

Davis–Putnam Algorithm sits in a sparse region of the domain-specific corpus (92^nd percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (2769 abstractions)

Nearest neighbors

• Resolution Proof Compression by Splitting — 0.79
• Modus Ponendo Tollens — 0.79
• Formal Theory — 0.79
• Negation as Failure — 0.79
• Fourier–Motzkin Elimination — 0.78

Computed from structural-signature embeddings · 2026-10-25