Davis–Putnam Algorithm¶

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

Version: v2 · 2026-09-06 · History
Domain-specific #: 1627
Origin domain: automated theorem proving
Subdomain: propositional satisfiability
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.^[1]

That satisfiability invariant is the algorithm's structural center. The procedure is not merely “use resolution until done.” It assigns resolution a specific eliminative role: construct the constraints that remain after existentially projecting one Boolean variable away. Pure-literal and unit-clause rules can simplify the clause set before or between eliminations. Elimination continues until either an empty clause appears, certifying contradiction, or no clauses remain, certifying satisfiability. Davis and Putnam introduced the procedure within a proof method for quantification theory; its finite propositional stage became a foundational SAT procedure.^[1]

The algorithm must be separated from the later Davis–Putnam–Logemann–Loveland procedure. DPLL replaces the potentially explosive exhaustive-resolution elimination step with case splitting and backtracking, while retaining unit propagation and related simplifications.^[2] They share a lineage and often share the abbreviation “DP” in historical discussion, but they are different algorithms.

Structural Signature¶

Clausal input: a finite set or multiset of propositional clauses, interpreted conjunctively.
Variable selection: a variable \(x\) is chosen for elimination.
Polarity partition: clauses containing \(x\), clauses containing \(\neg x\), and clauses containing neither are distinguished.
Resolution cross-product: each positive clause is resolved with each negative clause on \(x\).
Tautology deletion: resolvents containing both a literal and its negation are discarded.
Variable removal: all parent clauses containing either polarity of \(x\) are deleted.
Equisatisfiability invariant: the new clause set is satisfiable if and only if the old one is.
Simplification rules: unit clauses, pure literals, duplicate literals, and subsumed clauses may reduce work without changing the decision.
Terminal interpretation: an empty clause means unsatisfiable; an empty clause set means satisfiable.
Completeness with possible blow-up: finite elimination decides the input, but the number and size of resolvents may grow exponentially.

Recognition test. A procedure is Davis–Putnam only if its decisive progress operation is resolution-based variable elimination that removes both polarities after inserting the required resolvents. A solver that branches on \(x=0\) and \(x=1\) is following the DPLL line even if it also performs unit propagation.

What It Is Not¶

It is not generic resolution theorem proving. Resolution is the inference rule; Davis–Putnam is a particular finite procedure that organizes the rule around eliminating variables while maintaining a satisfiability invariant.

It is not DPLL. DPLL explores assignments by splitting and backtracking rather than forming all cross-polarity resolvents for each eliminated variable.^[2] Modern conflict-driven clause-learning solvers descend primarily from DPLL and add implication graphs, learned clauses, restarts, and heuristics.

It is not Gaussian elimination. Both remove variables, but Gaussian elimination operates over linear equations in a field and preserves an affine solution set. Davis–Putnam operates over disjunctive Boolean clauses and can change the model set while preserving only existence of a model.

It is not a heuristic SAT search. Given finite CNF input and faithful rule execution, it terminates with a correct SAT/UNSAT answer. Its weakness is worst-case resource growth, not logical incompleteness.

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.^[1]

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. The name should not be extended to arbitrary constraint elimination, first-order resolution without a finite ground reduction, or every solver that happens to simplify clauses.

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.

The transformation also clarifies what is preserved. Eliminating \(x\) generally does not preserve assignments one for one. It preserves whether at least one extension exists. A satisfying assignment to the reduced formula can be extended by a suitable truth value of \(x\), whereas restricting a satisfying assignment of the original formula to the remaining variables satisfies the resolvent closure. This bidirectional witness argument is why equisatisfiability, not syntactic equality, is the right invariant.

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. Repeating this can cause exponential growth. That problem motivated the DPLL replacement of wholesale elimination by splitting in machine implementations.^[2] Complexity management consequently depends on variable order and simplification, even though logical correctness does not.

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'\). If every \(A_i\) is true, choose \(x=0\); all positive parent clauses remain true through their \(A_i\), and all negative parent clauses are true through \(\neg x\). Otherwise some \(A_i\) is false; each resolvent forces every \(B_j\) true, so choose \(x=1\). This proves the existence-preserving step.

The proof reveals a useful conceptual reading: resolution elimination computes a CNF representation of existential projection \(\exists x\,F\). The algorithm iterates that projection until only the truth or falsity of the original existential satisfiability question remains.

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. The Davis–Putnam case is especially instructive because it shows how a weaker invariant than full equivalence can enable a decisive computation.

Examples¶

Consider

\[ (x\lor a)\land(x\lor b)\land(\neg x\lor c)\land(\neg x\lor d). \]

Eliminating \(x\) yields

\[ (a\lor c)\land(a\lor d)\land(b\lor c)\land(b\lor d). \]

The two formulas do not have the same variables or the same assignments, but they agree on whether a satisfying assignment exists.

For a contradiction, start with \(x\land\neg x\). Resolving the two unit clauses produces the empty clause, so the formula is unsatisfiable. By contrast, if the input is \((x\lor y)\land(\neg x\lor y)\), eliminating \(x\) produces the unit clause \(y\), accurately projecting the constraint onto the remaining variable.

A pure-literal example is \((x\lor a)\land(x\lor\neg b)\land c\). Because \(x\) appears only positively, assigning \(x=1\) satisfies every clause containing it; those clauses may be removed without resolution.

Structural Tensions¶

Progress versus clause growth: every elimination removes a variable but may multiply clauses. Diagnostic: count positive and negative occurrences before elimination and estimate the non-tautological resolvent cross-product.
Equisatisfiability versus model preservation: the decision survives while individual assignments may not. Diagnostic: ask whether reduced models need only extend to source models or must correspond bijectively.
Resolution elimination versus branching: both decide SAT but create different computation structures. Diagnostic: check whether the chosen variable disappears through all resolvents or is assigned in alternative branches.
Historical breadth versus modern scope: the 1960 procedure appears inside quantification theory, while the named algorithm is usually discussed as propositional CNF elimination. Diagnostic: identify the preprocessing and grounding stage before attributing first-order completeness to the finite clause step.
Completeness versus practicality: logical termination does not imply acceptable memory use. Diagnostic: separate proof of finite correctness from an empirical or asymptotic resource claim.

Structural–Framed Character¶

The Davis–Putnam algorithm is a formal structural abstraction. Its identity is fixed by clause roles, polarity, resolution, projection, simplification, and stopping conditions rather than by a specific program or institution. It is nevertheless framed by computational-logic vocabulary and cannot be recognized merely from the generic word “elimination.”

Its historical name is classificatory, not a claim that Davis and Putnam alone supplied every later SAT technique. The eponym identifies a particular procedural architecture.

Structural Core vs. Domain Accent¶

The structural core is variable removal by deriving residual constraints that preserve feasibility. The domain accent specifies Boolean literals, disjunctive clauses, complementary polarity, resolution, satisfiability, and the empty-clause convention.

Removing the accent leaves a broad elimination archetype. It does not recover the resolution rule or guarantee the equisatisfiability proof, so Davis–Putnam remains domain-specific rather than a new prime.

prime:algorithm is the minimal parent. Davis–Putnam is a finite, definite, effective procedure from CNF inputs to a SAT/UNSAT result, with correctness and termination obligations. It specializes Algorithm by fixing its representations, steps, invariant, and terminal certificates.

domain_specific:equisatisfiability is a constitutive invariant and close neighbor, not the genus: the relation can hold between formulas without any Davis–Putnam procedure. prime:deductive_reasoning supplies resolution's truth-preserving inferential background but is too broad to classify the algorithm.

Relationships to Other Abstractions¶

Current abstraction Davis–Putnam Algorithm Domain-specific

Parents (1) — more general patterns this builds on

Davis–Putnam Algorithm is a kind of Algorithm Prime

prime:algorithm is the minimal parent.

Hierarchy paths (2) — routes to 2 parentless roots

Davis–Putnam Algorithm → Algorithm → Function (Mapping)

Show alternative path (1)

Neighborhood in Abstraction Space¶

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

Family — Complexity Reductions & Decidability (10 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

DPLL: splitting-and-backtracking successor procedure.
Resolution: the inference rule used by the elimination step.
Unit propagation: one simplification rule, also used by many other solvers.
Variable elimination generally: a family spanning many algebras.
Tseitin transformation: a CNF encoding using fresh variables.
DP in dynamic programming: an unrelated abbreviation.

References¶

[1] Martin Davis and Hilary Putnam, “A Computing Procedure for Quantification Theory,” Journal of the ACM 7, no. 3 (1960): 201–215. https://doi.org/10.1145/321033.321034 registry ↩a ↩b ↩c

[2] Martin Davis, George Logemann, and Donald Loveland, “A Machine Program for Theorem-Proving,” Communications of the ACM 5, no. 7 (1962): 394–397. https://doi.org/10.1145/368273.368557 registry ↩a ↩b ↩c