evalCNF
The definition computes the truth value of a CNF formula under a given assignment by verifying that every clause holds. It is cited by proofs establishing satisfiability and by belief-propagation soundness arguments in the SAT encoding. The body is a direct application of the all quantifier over the clause list using the clause evaluator.
claimFor an assignment $a$ of $n$ Boolean variables and a CNF formula $φ$ consisting of a list of clauses, $evalCNF(a, φ)$ returns true if and only if $evalClause(a, C)$ holds for every clause $C$ in $φ$. The empty formula evaluates to true.
background
Variables are indexed by Fin n for a fixed problem size. An Assignment n is a function from variables to Boolean values. A CNF n is a structure containing a list of clauses. Clause evaluation is the disjunction over literals under the assignment. This definition supplies the top-level semantic map for CNF formulas, supporting consistency predicates and completeness results in the SAT layer.
proof idea
It is implemented as a one-line definition that applies the List.all predicate to the clauses of φ, invoking evalClause on each.
why it matters in Recognition Science
This supplies the evaluation function underlying Satisfiable and UniqueSolution. It is invoked in the soundness lemma for belief propagation steps and in lemmas constructing consistent states from satisfying assignments. It anchors the semantic layer of the SAT encoding within the Recognition Science complexity analysis.
scope and limits
- Does not compute the number of satisfying assignments.
- Does not restrict to 3-literal clauses.
- Does not address computational complexity of evaluation.
- Does not handle quantified Boolean formulas.
Lean usage
lemma sat_def {n} (φ : CNF n) : Satisfiable φ ↔ ∃ a, evalCNF a φ = true := by rflformal statement (Lean)
37def evalCNF {n} (a : Assignment n) (φ : CNF n) : Bool :=
proof body
Definition body.
38 φ.clauses.all (fun C => evalClause a C)
39
40/-- Satisfiable CNF. -/