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.

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) — 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

• Modus Ponendo Tollens — 0.79
• Formal Theory — 0.79
• Negation as Failure — 0.79
• Fourier–Motzkin Elimination — 0.78
• Algebraic Decision Diagram — 0.77

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