valueOfClause
plain-language theorem explainer
valueOfClause computes the boolean value of a clause under a partial assignment by evaluating all its literals and returning the disjunction only when every literal is determined. Researchers building SAT backpropagation algorithms cite this when implementing clause satisfaction checks in partial assignments. The definition maps literals via the companion literal evaluator then applies an all-known check before computing the any-true result.
Claim. Given a partial assignment $σ$ from variables to optional booleans and a clause $C$ as a list of literals, the clause value is $some(b)$ if every literal evaluates to a definite boolean under $σ$, where $b$ is the logical disjunction of those values, and $none$ otherwise.
background
PartialAssignment n is the type of functions from variable indices to Option Bool, where none signals an undetermined variable. Clause n is defined as a list of literals in the CNF module. The module develops partial assignments for backpropagation over CNF formulas that may include XOR constraints, supplying clause and literal evaluators as primitives. The literal evaluator valueOfLit handles positive and negative polarities by direct lookup or negation.
proof idea
The definition constructs the list of literal values by mapping the clause through valueOfLit. It checks completeness with the all predicate on Option.isSome. When all values are present it returns some of the any-true computation over the list; otherwise it yields none.
why it matters
This definition supplies the clause evaluation step required for backpropagation in SAT instances. It forms part of the machinery for steps such as BPStep and completeness checks within the module. No immediate parent theorems are recorded, but it enables modeling of constraint propagation in the Recognition framework's complexity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.