BPState
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not embed the CNF formula or XOR system.
- Does not define any propagation rules or update functions.
- Does not assert consistency or completeness of the assignment.
- Does not impose ordering or selection heuristics on variables.
formal statement (Lean)
13structure BPState (n : Nat) where
14 assign : PartialAssignment n
15
16/-- Update a partial assignment at variable `v` to value `b`. -/