evalClause
plain-language theorem explainer
The definition returns true for a clause under an assignment precisely when at least one literal is satisfied. SAT encoding layers and backpropagation soundness arguments cite it to fix the meaning of clause satisfaction. It is realized as a direct one-line application of the list any combinator to the literal evaluator.
Claim. Let $a$ be a total assignment of truth values to $n$ variables and let $C$ be a finite list of literals. Then $evalClause(a,C)$ equals true if and only if there exists $l$ in $C$ such that $evalLit(a,l)$ holds, and equals false when $C$ is empty.
background
Variables are indexed by Fin n. An Assignment n is a function Var n to Bool supplying a complete truth assignment. A Clause n is a list of Lit n, each literal being either positive or negative. The upstream evalLit maps a positive literal to the variable value and a negative literal to its negation. This supplies the local semantics for SAT problems inside the CNF module.
proof idea
The definition is a one-line wrapper that applies the any combinator to the clause list, delegating each literal test to evalLit.
why it matters
It supplies the satisfaction predicate for single clauses and is invoked by evalCNF to evaluate full CNF formulas. It is used in bp_step_sound and clauseUnit_correct for backpropagation soundness and in satisfiesConstraint for mixed constraint semantics. The declaration therefore anchors the clause layer of the SAT encoding used throughout the complexity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.