Correctness of the DPLL solver

TheoremCorrectness of DPLL with sufficient fuel#✓fully proved

Let \(\varphi\) be a CNF formula and let \(n\) be a natural number at least the number of distinct variables occurring in \(\varphi\). Then DPLL with fuel \(n\) returns true on \(\varphi\) if and only if \(\varphi\) is satisfiable.

theorem decideWithFuel_eq_true_iff {fuel : Nat} {formula : CNF}
    (hfuel : formula.vars.card ≤ fuel) :
    decideWithFuel fuel formula = true ↔ CNFSat formula

Uses 15 · Used by 1

Statement usesDPLL with a fuel budget · CNF formula · Variables of a CNF formula · Satisfiability of a CNF formula

Proof usesFirst unit literal · First variable of a CNF formula · Satisfaction of a CNF formula · Restriction reduces the number of variables · Restriction of a CNF formula by a literal · Unit propagation preserves satisfiability · Splitting on a variable · CNF clause · Satisfaction of a clause · Variables of a clause · Satisfiability means having a satisfying assignment

Used byCorrectness of DPLL

TheoremCorrectness of DPLL#✓fully proved

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

theorem dpll_eq_true_iff {formula : CNF} :
    dpll formula = true ↔ CNFSat formula

Uses 5 · Used by 1

Statement usesThe DPLL procedure · CNF formula · Satisfiability of a CNF formula

Proof usesCorrectness of DPLL with sufficient fuel · Variables of a CNF formula

Used byCorrectness of the fixed-length SAT-backed solver

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.