BPState
plain-language theorem explainer
BPState packages a partial assignment as the working state for backward propagation over CNF formulas with XOR constraints. Researchers analyzing SAT solvers or constraint propagation in the Recognition framework cite it when defining states for step relations and completeness arguments. The declaration is a direct structure wrapper around the PartialAssignment function type with no additional fields or computation.
Claim. A backpropagation state over $n$ variables is a record whose single field is a partial assignment $a : V_n → Option(Bool)$, where $V_n$ denotes the set of variables and $Option(Bool)$ encodes undetermined ($none$) or fixed ($some b$) values.
background
The module treats partial assignments as the core representation during backpropagation: each variable is either unknown ($none$) or determined to a Boolean value ($some b$). BPState simply wraps this function type into a named structure so that subsequent inductive relations and predicates can refer to it uniformly.
proof idea
The declaration is a structure definition with one field of type PartialAssignment n. It is introduced by direct record construction with no tactics or lemmas applied.
why it matters
BPState is the central carrier for the backpropagation machinery. It is used by BackpropSucceeds (every legal start reaches a complete consistent state), BPStep (the guarded propagation relation), bp_step_monotone, bp_step_sound, complete, and consistent. These in turn support the completeness results in the SAT module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.