Decoded CNF literal evaluation equals satisfiesB

Proved

CookLevin.decodeFormula_all_literals_eq_satisfiesB

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

cnfcook-levinevaluatorsat-verifier

For every encoded CNF string $x$ and Boolean assignment string $w$ , explicitly evaluating every decoded clause by scanning its literals yields exactly the Boolean satisfaction predicate $\operatorname{satisfiesB}$ applied to the decoded assignment and formula.

This bridge identifies the concrete nested all/any evaluator implemented by a machine with the semantic CNF evaluator used by the SAT verifier.

Formal statement

import Definitions.Def_CookLevin_Verifier
open CookLevin

theorem CookLevin.decodeFormula_all_literals_eq_satisfiesB (x w : List Bool) :
    (decodeFormula x).all (fun clause =>
      clause.any (fun lit => match lit with
        | Literal.Neg n => !(w.getD n false)
        | Literal.Pos n => w.getD n false)) =
      satisfiesB (decodeAssignment w) (decodeFormula x) := by sorry

Source

Decomposition of CookLevin.satisfiesB_machine_product: https://prove2.me/theorems/7bed476e-8ddf-42a1-9927-dc459719322c; definitions in Def_CookLevin_Verifier

View graph