SAT and bounded string constraints: reduction correctness

DefinitionEncoding of CNF formulas as string constraints#✓fully proved

SAT as string constraints: each clause is a disjunction of word equations x = [b], one per literal.

def encodeCNF (φ : CNF) : Formula Bool ℕ :=
  andChain (φ.map (fun C =>
    orChain (C.map (fun l =>
      Formula.atom (Atom.eq (Term.var l.1) (Term.const [l.2]))))))

Uses 7 · Used by 2

Statement usesString constraint atom · String formulas · String term over variables · Conjunction of a list of string formulas · Disjunction of a list of string formulas · CNF formula · CNF clause

Used bySAT iff the bounded-search specification holds of the encoding · Correctness of the SAT-to-string-constraints translation

TheoremCorrectness of the SAT-to-string-constraints translation#✓fully proved

Correctness of the SAT-to-string-constraints translation at length bound 1: Boolean assignments become length-≤ 1 string assignments and back.

theorem cnfSat_iff_stringSat (φ : CNF) :
    CNFSat φ ↔ ∃ σ : ℕ → List Bool, (∀ i, (σ i).length ≤ 1) ∧
      Sat σ (encodeCNF φ)

Uses 13 · Used by 1

Statement usesSatisfaction of a string formula · Encoding of CNF formulas as string constraints · CNF formula · Satisfiability of a CNF formula

Proof usesString constraint atom · String formulas · String term over variables · Conjunction of a list of string formulas · Evaluation of a string term under an assignment · Disjunction of a list of string formulas · Satisfaction of a conjunction chain · Satisfaction of a disjunction chain · CNF clause

Used bySAT iff the bounded-search specification holds of the encoding

TheoremSAT iff the bounded-search specification holds of the encoding#✓fully proved

SAT iff the bounded-search specification holds of the encoding at length bound 1, for any variable list covering the variables of the encoding. This is the bridge from the reduction to the bounded-search specification: boundedSatSpec_iff (soundness / completeness of the finite search) plus the reduction correctness.

theorem cnfSat_iff_boundedSatSpec (φ : CNF) (vs : List ℕ)
    (hvars : ∀ i ∈ varsOfFormula (encodeCNF φ), i ∈ vs) :
    CNFSat φ ↔ boundedSatSpec vs (encodeCNF φ) 1 = true

Uses 9

Statement usesBounded-search satisfiability specification · Encoding of CNF formulas as string constraints · Variables occurring in a string formula · CNF formula · Satisfiability of a CNF formula

Proof usesSatisfaction of a string formula · Soundness and completeness of the bounded-search specification · Correctness of the SAT-to-string-constraints translation · Formula satisfaction depends only on its variables

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.