Bit-blasting word equations to the verified DPLL solver

DefinitionSAT variable index for a bit of a string variable#✓fully proved

A positive SAT index for position p of variable i; 0 is reserved.

def bitVar (i p : ℕ) : ℕ := Nat.pair i p + 1

Used by 4

Used byBit-blasting a word into literals · Linear size bound for bit-blasted words · Fixed-length bit-blasting is equisatisfiable · Decoding string values from a SAT assignment

DefinitionBit-blasting a word into literals#✓fully proved

Expand a word into literals at a fixed length for each string variable.

def blastWord (ℓ : Fin n → ℕ) (w : List (Bool ⊕ Fin n)) : List (ℕ × Bool) :=
  w.flatMap fun
    | .inl b => [(0, b)]
    | .inr i => List.ofFn (fun p : Fin (ℓ i) => (bitVar i.val p.val, true))

Uses 1 · Used by 5

Statement usesSAT variable index for a bit of a string variable

Used byCNF encoding of a word-equation system at fixed lengths · Exact clause count of the CNF encoding · CNF encoding uses clauses of width at most two · Linear size bound for bit-blasted words · Fixed-length bit-blasting is equisatisfiable

DefinitionClauses forcing two literals to be equal#✓fully proved

Two implication clauses forcing equal truth values of two literals.

def iffClauses (a b : ℕ × Bool) : CNF :=
  [[(a.1, !a.2), b], [(b.1, !b.2), a]]

Uses 2 · Used by 3

Statement usesCNF formula · CNF clause

Used byCNF encoding uses clauses of width at most two · Fixed-length bit-blasting is equisatisfiable · Position-wise equality clauses for literal vectors

DefinitionPosition-wise equality clauses for literal vectors#✓fully proved

Compare literal vectors position by position; a length mismatch emits an empty clause.

def equalWordClauses : List (ℕ × Bool) → List (ℕ × Bool) → CNF
  | [], [] => []
  | a :: as, b :: bs => iffClauses a b ++ equalWordClauses as bs
  | _, _ => [[]]

Uses 3 · Used by 4

Statement usesClauses forcing two literals to be equal · CNF formula · CNF clause

Used byCNF encoding uses clauses of width at most two · Fixed-length bit-blasting is equisatisfiable · Clauses for a word equation with a length check · Clause count for one word equation

DefinitionClauses for a word equation with a length check#✓fully proved

Short-circuit unequal lengths before emitting position-wise equality clauses.

def equationClauses (as bs : List (ℕ × Bool)) : CNF :=
  if as.length = bs.length then equalWordClauses as bs else [[]]

Uses 3 · Used by 5

Statement usesPosition-wise equality clauses for literal vectors · CNF formula · CNF clause

Used byCNF encoding of a word-equation system at fixed lengths · Exact clause count of the CNF encoding · CNF encoding uses clauses of width at most two · Fixed-length bit-blasting is equisatisfiable · Clause count for one word equation

DefinitionCNF encoding of a word-equation system at fixed lengths#✓fully proved

CNF for a system at fixed lengths, with shared variables and one constant bit.

def blastSystem (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) : CNF :=
  [(0, true)] :: eqs.flatMap (fun e =>
    equationClauses (blastWord ℓ e.lhs) (blastWord ℓ e.rhs))

Uses 5 · Used by 5

Statement usesOrdinary word equation · Bit-blasting a word into literals · Clauses for a word equation with a length check · CNF formula · CNF clause

Used byExact clause count of the CNF encoding · CNF encoding uses clauses of width at most two · Fixed-length bit-blasting is equisatisfiable · Fixed-length word-equation solver via DPLL · Correctness of the fixed-length SAT-backed solver

DefinitionDecoding string values from a SAT assignment#✓fully proved

Read each string variable's bits from a SAT assignment.

def decodeAssignment (ℓ : Fin n → ℕ) (v : ℕ → Bool) (i : Fin n) : List Bool :=
  List.ofFn (fun p : Fin (ℓ i) => v (bitVar i.val p.val))

Uses 1 · Used by 1

Statement usesSAT variable index for a bit of a string variable

Used byFixed-length bit-blasting is equisatisfiable

DefinitionEncoding a substitution as a SAT assignment#✓fully proved

Encode a substitution as a total SAT assignment, using inverse pairing.

def encodeAssignment (σ : Fin n → List Bool) (x : ℕ) : Bool :=
  if x = 0 then true
  else if h : (Nat.unpair (x - 1)).1 < n then
    (σ ⟨(Nat.unpair (x - 1)).1, h⟩).getD (Nat.unpair (x - 1)).2 false
  else false

Used by 1

Used byFixed-length bit-blasting is equisatisfiable

TheoremFixed-length bit-blasting is equisatisfiable#✓fully proved

Fixed-length bit-blasting is satisfiability-preserving in both directions.

theorem cnfSat_blastSystem (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) :
    CNFSat (blastSystem ℓ eqs) ↔
      ∃ σ : Fin n → List Bool, (∀ i, (σ i).length = ℓ i) ∧
        ∀ e ∈ eqs, e.Satisfies σ

Uses 18 · Used by 1

Statement usesOrdinary word equation · Solution of a word equation · CNF encoding of a word-equation system at fixed lengths · Satisfiability of a CNF formula

Proof usesSAT variable index for a bit of a string variable · Bit-blasting a word into literals · Decoding string values from a SAT assignment · Encoding a substitution as a SAT assignment · Position-wise equality clauses for literal vectors · Clauses for a word equation with a length check · Substitution of words for variables in a word · Clauses forcing two literals to be equal · CNF formula · Satisfaction of a CNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · Satisfiability means having a satisfying assignment

Used byCorrectness of the fixed-length SAT-backed solver

DefinitionFixed-length word-equation solver via DPLL#✓fully proved

Solve the fixed-length system by bit-blasting and the verified DPLL solver.

def fixedLengthSatB (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) : Bool :=
  Cslib.Algorithms.SAT.DPLL.dpll (blastSystem ℓ eqs)

Uses 3 · Used by 3

Statement usesThe DPLL procedure · Ordinary word equation · CNF encoding of a word-equation system at fixed lengths

Used byBounded word-equation solver via DPLL · Soundness and completeness of the bounded word-equation solver · Correctness of the fixed-length SAT-backed solver

TheoremCorrectness of the fixed-length SAT-backed solver#✓fully proved

The executable SAT-backed procedure accepts exactly the fixed-length solutions.

theorem fixedLengthSatB_iff (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) :
    fixedLengthSatB ℓ eqs = true ↔
      ∃ σ : Fin n → List Bool, (∀ i, (σ i).length = ℓ i) ∧
        ∀ e ∈ eqs, e.Satisfies σ

Uses 8 · Used by 1

Statement usesOrdinary word equation · Solution of a word equation · Fixed-length word-equation solver via DPLL

Proof usesThe DPLL procedure · Correctness of DPLL · CNF encoding of a word-equation system at fixed lengths · Fixed-length bit-blasting is equisatisfiable · Satisfiability of a CNF formula

Used bySoundness and completeness of the bounded word-equation solver

DefinitionEnumeration of bounded length profiles#✓fully proved

All bounded length profiles, using Mathlib's finite Cartesian-product enumeration.

def lengthProfiles (n B : ℕ) : List (Fin n → ℕ) :=
  ((List.finRange n).pi (fun _ => List.range (B + 1))).map
    (fun f i => f i (List.mem_finRange i))

Used by 4

Used byBounded word-equation solver via DPLL · Soundness and completeness of the bounded word-equation solver · Size of the length-profile search · Membership in the length-profile enumeration

TheoremMembership in the length-profile enumeration#✓fully proved

The profile enumeration contains exactly the pointwise-bounded length assignments.

theorem mem_lengthProfiles (ℓ : Fin n → ℕ) (B : ℕ) :
    ℓ ∈ lengthProfiles n B ↔ ∀ i, ℓ i ≤ B

Uses 1 · Used by 1

Statement usesEnumeration of bounded length profiles

Used bySoundness and completeness of the bounded word-equation solver

DefinitionBounded word-equation solver via DPLL#✓fully proved

Solve bounded word equations by trying finite length profiles and calling DPLL.

def boundedWordSatB (B : ℕ) (eqs : List (WordEq Bool (Fin n))) : Bool :=
  (lengthProfiles n B).any (fun ℓ => fixedLengthSatB ℓ eqs)

Uses 3 · Used by 6

Statement usesOrdinary word equation · Fixed-length word-equation solver via DPLL · Enumeration of bounded length profiles

Used bySAT backend agrees with the bounded formula semantics · Soundness and completeness of the bounded word-equation solver · Decision procedure for bounded Boolean word equations · Pattern-matching decision against a concrete target · Target length bounds the pattern-matching search · Satisfiability as acceptance by some bounded SAT search

TheoremSoundness and completeness of the bounded word-equation solver#✓fully proved

The bounded SAT-backed solver is sound and complete, including empty strings.

theorem boundedWordSatB_iff (B : ℕ) (eqs : List (WordEq Bool (Fin n))) :
    boundedWordSatB B eqs = true ↔
      ∃ σ : Fin n → List Bool, (∀ i, (σ i).length ≤ B) ∧
        ∀ e ∈ eqs, e.Satisfies σ

Uses 7 · Used by 4

Statement usesOrdinary word equation · Solution of a word equation · Bounded word-equation solver via DPLL

Proof usesFixed-length word-equation solver via DPLL · Correctness of the fixed-length SAT-backed solver · Enumeration of bounded length profiles · Membership in the length-profile enumeration

Used bySAT backend agrees with the bounded formula semantics · Decision procedure for bounded Boolean word equations · Target length bounds the pattern-matching search · Satisfiability as acceptance by some bounded SAT search

DefinitionDecision procedure for bounded Boolean word equations#✓fully proved

An executable decision procedure for bounded Boolean-alphabet word equations.

def decidableBoundedWordEq (B : ℕ) (eqs : List (WordEq Bool (Fin n))) :
    Decidable (∃ σ : Fin n → List Bool, (∀ i, (σ i).length ≤ B) ∧
      ∀ e ∈ eqs, e.Satisfies σ) :=
  decidable_of_iff (boundedWordSatB B eqs = true) (boundedWordSatB_iff B eqs)

Uses 4

Statement usesOrdinary word equation · Solution of a word equation · Bounded word-equation solver via DPLL · Soundness and completeness of the bounded word-equation solver

TheoremSize of the length-profile search#✓fully proved

The complete length-profile search has (B + 1)^n entries.

theorem lengthProfiles_length (n B : ℕ) : (lengthProfiles n B).length = (B + 1) ^ n

Uses 1

Statement usesEnumeration of bounded length profiles

TheoremClause count for one word equation#✓fully proved

One empty clause for unequal lengths; otherwise two clauses per bit.

theorem equationClauses_length (as bs : List (ℕ × Bool)) :
    (equationClauses as bs).length =
      if as.length = bs.length then 2 * as.length else 1

Uses 4 · Used by 1

Statement usesClauses for a word equation with a length check · CNF clause

Proof usesPosition-wise equality clauses for literal vectors · CNF formula

Used byExact clause count of the CNF encoding

TheoremExact clause count of the CNF encoding#✓fully proved

Exact CNF size: one constant-bit clause plus the position clauses for every equation. This is an output-size count, not a TimeM or DPLL runtime bound.

theorem blastSystem_length (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) :
    (blastSystem ℓ eqs).length = 1 + (eqs.map (fun e =>
      if (blastWord ℓ e.lhs).length = (blastWord ℓ e.rhs).length
      then 2 * (blastWord ℓ e.lhs).length else 1)).sum

Uses 6

Statement usesOrdinary word equation · CNF encoding of a word-equation system at fixed lengths · Bit-blasting a word into literals · CNF clause

Proof usesClauses for a word equation with a length check · Clause count for one word equation

TheoremCNF encoding uses clauses of width at most two#✓fully proved

Every emitted clause has at most two literals, including the constant unit clause.

theorem blastSystem_width (ℓ : Fin n → ℕ) (eqs : List (WordEq Bool (Fin n))) :
    ∀ c ∈ blastSystem ℓ eqs, c.length ≤ 2

Uses 8

Statement usesOrdinary word equation · CNF encoding of a word-equation system at fixed lengths · CNF formula · CNF clause

Proof usesBit-blasting a word into literals · Position-wise equality clauses for literal vectors · Clauses for a word equation with a length check · Clauses forcing two literals to be equal

TheoremSatisfiability as acceptance by some bounded SAT search#✓fully proved

A source system is satisfiable iff some bounded SAT search accepts. This does not make failure at one bound a decision of general UNSAT.

theorem wordSystem_satisfiable_iff_exists_boundedSatB (eqs : List (WordEq Bool (Fin n))) :
    (∃ σ : Fin n → List Bool, ∀ e ∈ eqs, e.Satisfies σ) ↔
      ∃ B : ℕ, boundedWordSatB B eqs = true

Uses 5

Statement usesOrdinary word equation · Solution of a word equation · Bounded word-equation solver via DPLL

Proof usesSoundness and completeness of the bounded word-equation solver · Solvability of word equation systems at a finite length bound

DefinitionPattern-matching decision against a concrete target#✓fully proved

Decide matching against a concrete target, with no bound supplied by the caller.

def patternMatchB (w : List (Bool ⊕ Fin n)) (target : List Bool) : Bool :=
  boundedWordSatB target.length [⟨w, target.map Sum.inl⟩]

Uses 2 · Used by 2

Statement usesOrdinary word equation · Bounded word-equation solver via DPLL

Used byDecidability of Boolean-word pattern matching · Target length bounds the pattern-matching search

TheoremTarget length bounds the pattern-matching search#✓fully proved

The target length is a sufficient search bound for unrestricted pattern matching.

theorem patternMatchB_iff (w : List (Bool ⊕ Fin n)) (target : List Bool) :
    patternMatchB w target = true ↔ ∃ σ : Fin n → List Bool, evalWord σ w = target

Uses 7 · Used by 1

Statement usesSubstitution of words for variables in a word · Pattern-matching decision against a concrete target

Proof usesOrdinary word equation · Solution of a word equation · Bounded word-equation solver via DPLL · Soundness and completeness of the bounded word-equation solver · Bounding variable images by the target loses no pattern matches

Used byDecidability of Boolean-word pattern matching

DefinitionDecidability of Boolean-word pattern matching#✓fully proved

Executable decidability for unrestricted Boolean-word pattern matching.

def decidablePatternMatch (w : List (Bool ⊕ Fin n)) (target : List Bool) :
    Decidable (∃ σ : Fin n → List Bool, evalWord σ w = target) :=
  decidable_of_iff (patternMatchB w target = true) (patternMatchB_iff w target)

Uses 3

Statement usesSubstitution of words for variables in a word · Pattern-matching decision against a concrete target · Target length bounds the pattern-matching search

TheoremLinear size bound for bit-blasted words#✓fully proved

Expanded words are at most linear in source-word length and the supplied bound. Together with blastSystem_length, this bounds CNF output size, not solver time.

theorem blastWord_length_le (ℓ : Fin n → ℕ) (w : List (Bool ⊕ Fin n)) (B : ℕ)
    (h : ∀ i, ℓ i ≤ B) : (blastWord ℓ w).length ≤ max 1 B * w.length

Uses 2

Statement usesBit-blasting a word into literals

Proof usesSAT variable index for a bit of a string variable

TheoremSAT backend agrees with the bounded formula semantics#✓fully proved

The SAT backend decides the same bounded semantics as the existing formula language.

theorem boundedWordSatB_formula_iff (B : ℕ) (eqs : List (WordEq Bool (Fin n))) :
    boundedWordSatB B eqs = true ↔
      ∃ σ : Fin n → List Bool, (∀ i, (σ i).length ≤ B) ∧
        Sat σ (andChain (eqs.map WordEq.toFormula))

Uses 10

Statement usesString formulas · Satisfaction of a string formula · Ordinary word equation · Word equation as a string-constraint formula · Conjunction of a list of string formulas · Bounded word-equation solver via DPLL

Proof usesSolution of a word equation · Formula embedding of word equations preserves satisfaction · Soundness and completeness of the bounded word-equation solver · Satisfaction of a conjunction chain

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.