Reference · The Applied Higher-Order Functions catalogue

rainbow.algorithms.proofs.ahof.sat

The Applied Higher-Order Functions cataloguesrc/rainbow/algorithms/proofs/ahof/sat.clj1 definitions, 4 theorems

AHoF V50 SAT-based Bounded Model Checking: the system is unrolled k steps and encoded as a boolean formula in CNF; a counterexample exists iff the formula is satisfiable. The core evaluation is clause satisfaction under a truth assignment -- a clause (disjunction of literals) is satisfied when at least one of its literals is true: clause-satisfied? literals = fold or false literals. Proved native and axiom-free (a boolean fold via data/List.rec + logic/if-data, no rational arithmetic): the fold, its cons recurrence, and worked clauses. A full CNF formula is satisfied when every clause is; the SAT search itself and the unrolling encoding are executable concerns; what is proved here is the clause-satisfaction evaluation. Requires data/Bool, data/List.rec, and logic/if-data (all in the D63 checkpoint). Scope (measured by the kernel): this module has 3 worked instances (statements about specific values) and 1 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.ahof.sat` prints this classification.

sat/clause-satisfied? :
  (x₁ : List data/Bool)
  → data/Bool

sat/clause-cons :
  (head : data/Bool) (tail : List data/Bool)
  → sat/clause-satisfied? (data/cons data/Bool head tail) = logic/if-data data/Bool (head = head) head data/true (sat/clause-satisfied? tail)

sat/clause-satisfiable :
  → sat/clause-satisfied? [data/false, data/true, data/false] = data/true

sat/clause-unsatisfiable :
  → sat/clause-satisfied? [data/false, data/false] = data/false

sat/clause-empty :
  → sat/clause-satisfied? [] = data/false