Davis–Putnam algorithm

DefinitionClauses containing a variable only positively#✓fully proved

For a variable \(x\) and a CNF formula \(\varphi\), the formula consisting of the clauses of \(\varphi\), in their order, that contain the literal \(x\) and do not contain the literal \(\neg x\).

def posClauses (x : Nat) (φ : CNF) : CNF :=
  φ.filter fun C ↦ (x, true) ∈ C ∧ (x, false) ∉ C

Uses 2 · Used by 4

Statement usesCNF formula · CNF clause

Used byCorrectness of the Davis-Putnam procedure · Davis-Putnam elimination of a variable · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step

DefinitionClauses containing a variable only negatively#✓fully proved

For a variable \(x\) and a CNF formula \(\varphi\), the formula consisting of the clauses of \(\varphi\), in their order, that contain the literal \(\neg x\) and do not contain the literal \(x\).

def negClauses (x : Nat) (φ : CNF) : CNF :=
  φ.filter fun C ↦ (x, false) ∈ C ∧ (x, true) ∉ C

Uses 2 · Used by 4

Statement usesCNF formula · CNF clause

Used byCorrectness of the Davis-Putnam procedure · Davis-Putnam elimination of a variable · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step

DefinitionDavis-Putnam elimination of a variable#✓fully proved

Eliminating a variable \(x\) from a CNF formula \(\varphi\) gives the formula consisting of the clauses of \(\varphi\) that contain neither \(x\) nor \(\neg x\), followed by the resolvents on \(x\) of \(C\) and \(D\), for every clause \(C\) of \(\varphi\) that contains \(x\) but not \(\neg x\) and every clause \(D\) of \(\varphi\) that contains \(\neg x\) but not \(x\). Clauses containing both \(x\) and \(\neg x\) are dropped.

def eliminate (x : Nat) (φ : CNF) : CNF :=
  let neg := negClauses x φ
  φ.filter (fun C ↦ (x, true) ∉ C ∧ (x, false) ∉ C) ++
    (posClauses x φ).flatMap fun C ↦ neg.map fun D ↦ CNFClause.resolvent x C D

Uses 5 · Used by 5

Statement usesCNF formula · Clauses containing a variable only negatively · Clauses containing a variable only positively · CNF clause · Resolvent of two clauses

Used byDavis-Putnam elimination preserves satisfiability · Correctness of the Davis-Putnam procedure · Successive elimination of a list of variables · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step

TheoremResolvents do not mention the resolved variable#✓fully proved

Let \(x\) be a variable and let \(C\) and \(D\) be clauses such that \(C\) does not contain \(\neg x\) and \(D\) does not contain \(x\). Then no literal of the resolvent of \(C\) and \(D\) on \(x\) has variable \(x\).

In particular, the resolvents added when eliminating \(x\) do not mention \(x\).

theorem fst_ne_of_mem_resolvent {x : Nat} {C D : CNFClause} (hC : (x, false) ∉ C)
    (hD : (x, true) ∉ D) {l : Nat × Bool} (hl : l ∈ CNFClause.resolvent x C D) : l.1 ≠ x

Uses 2 · Used by 2

Statement usesCNF clause · Resolvent of two clauses

Used byCorrectness of the Davis-Putnam procedure · Completeness of a Davis-Putnam step

TheoremSoundness of a Davis-Putnam step#✓fully proved

Let \(x\) be a variable and \(\varphi\) a CNF formula. Every assignment that satisfies \(\varphi\) also satisfies the formula obtained from \(\varphi\) by eliminating \(x\).

theorem satisfies_eliminate {x : Nat} {φ : CNF} {σ : Nat → Bool} (h : φ.Satisfies σ) :
    (eliminate x φ).Satisfies σ

Uses 9 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · Davis-Putnam elimination of a variable

Proof usesClauses containing a variable only negatively · Clauses containing a variable only positively · CNF clause · Satisfaction of a clause · Resolvent of two clauses · Resolution rule soundness

Used byDavis-Putnam elimination preserves satisfiability

TheoremCompleteness of a Davis-Putnam step#✓fully proved

Let \(x\) be a variable, \(\varphi\) a CNF formula and \(\sigma\) an assignment that satisfies the formula obtained from \(\varphi\) by eliminating \(x\). Then there is a truth value \(b\) such that the assignment that agrees with \(\sigma\) except that it sends \(x\) to \(b\) satisfies \(\varphi\).

theorem exists_satisfies_update_of_satisfies_eliminate {x : Nat} {φ : CNF} {σ : Nat → Bool}
    (h : (eliminate x φ).Satisfies σ) : ∃ b, φ.Satisfies (Function.update σ x b)

Uses 10 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · Davis-Putnam elimination of a variable

Proof usesResolvents do not mention the resolved variable · Clauses containing a variable only negatively · Clauses containing a variable only positively · CNF clause · Satisfaction of a clause · Resolvent of two clauses · Satisfaction of a literal

Used byDavis-Putnam elimination preserves satisfiability

TheoremDavis-Putnam elimination preserves satisfiability#✓fully proved

For every variable \(x\) and every CNF formula \(\varphi\), the formula obtained from \(\varphi\) by eliminating \(x\) is satisfiable if and only if \(\varphi\) is satisfiable.

theorem cnfSat_eliminate_iff (x : Nat) (φ : CNF) : CNFSat (eliminate x φ) ↔ CNFSat φ

Uses 7 · Used by 1

Statement usesCNF formula · Davis-Putnam elimination of a variable · Satisfiability of a CNF formula

Proof usesSatisfaction of a CNF formula · Completeness of a Davis-Putnam step · Soundness of a Davis-Putnam step · Satisfiability means having a satisfying assignment

Used byCorrectness of the Davis-Putnam procedure

DefinitionSuccessive elimination of a list of variables#✓fully proved

Given a list \(x_1, \dots, x_n\) of variables and a CNF formula \(\varphi\), eliminate \(x_1\) from \(\varphi\), then \(x_2\) from the result, and so on up to \(x_n\). For the empty list the result is \(\varphi\).

def eliminateAll : List Nat → CNF → CNF
  | [], φ => φ
  | x :: xs, φ => eliminateAll xs (eliminate x φ)

Uses 2 · Used by 2

Statement usesCNF formula · Davis-Putnam elimination of a variable

Used byThe Davis-Putnam procedure · Correctness of the Davis-Putnam procedure

DefinitionVariable list for Davis–Putnam elimination#✓fully proved

For a CNF formula \(\varphi\), the list of the variables occurring in the literals of \(\varphi\), each listed exactly once, in order of first occurrence when the clauses of \(\varphi\), and the literals within each clause, are read from left to right.

Removing the repetitions takes time quadratic in the number of literal occurrences, which the eliminations dominate.

def varList (φ : CNF) : List Nat := (φ.flatMap (List.map Prod.fst)).eraseDups

Uses 1 · Used by 2

Statement usesCNF formula

Used byThe Davis-Putnam procedure · Correctness of the Davis-Putnam procedure

DefinitionThe Davis-Putnam procedure#✓fully proved

Given a CNF formula \(\varphi\), eliminate the variables that occur in \(\varphi\) one after another, each exactly once, in the order of their first occurrence in \(\varphi\), each elimination being applied to the result of the previous one. The procedure returns true if the resulting formula does not contain the empty clause, and false if it does.

def davisPutnam (φ : CNF) : Bool := decide ([] ∉ eliminateAll (varList φ) φ)

Uses 4 · Used by 1

Statement usesCNF formula · Successive elimination of a list of variables · Variable list for Davis–Putnam elimination · CNF clause

Used byCorrectness of the Davis-Putnam procedure

TheoremCorrectness of the Davis-Putnam procedure#✓fully proved

For every CNF formula \(\varphi\), the Davis-Putnam procedure returns true on \(\varphi\) if and only if \(\varphi\) is satisfiable.

theorem davisPutnam_eq_true_iff (φ : CNF) : davisPutnam φ = true ↔ CNFSat φ

Uses 18

Statement usesCNF formula · The Davis-Putnam procedure · Satisfiability of a CNF formula

Proof usesSatisfaction of a CNF formula · Davis-Putnam elimination preserves satisfiability · Davis-Putnam elimination of a variable · Successive elimination of a list of variables · Resolvents do not mention the resolved variable · Clauses containing a variable only negatively · Unsatisfiable formulas without variables contain the empty clause · Clauses containing a variable only positively · Variable list for Davis–Putnam elimination · Variables of a CNF formula · CNF clause · Satisfaction of a clause · Resolvent of two clauses · Variables of a clause · Satisfiability means having a satisfying assignment

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.