BPStep
BPStep is the inductive relation that encodes the allowed single-step transitions of a backpropagation procedure on partial assignments for a CNF formula together with an XOR constraint system. Researchers analyzing propagation-based SAT solvers or completeness arguments in Recognition Science would cite the definition when establishing monotonicity or soundness of individual steps. The relation is introduced directly by a list of guarded constructors that cover XOR value pushes, unit-clause resolutions, and identity steps for gate operations.
claimLet $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system over the same variables. For partial-assignment states $s$ and $t$, the relation BPStep($φ$, $H$, $s$, $t$) holds when $t$ is obtained from $s$ by one of the following: (i) an XOR constraint in $H$ supplies a unique missing variable-value pair, (ii) a clause of $φ$ is a unit clause under the current assignment and supplies its forced value, or (iii) the state is left unchanged by one of the placeholder gate rules (AND, OR, NOT, wire).
background
BPState is the structure whose only field is an assignment of type PartialAssignment $n$, where each variable is mapped to either none (unknown) or some Boolean value (determined). The module works with partial assignments for backpropagation, treating none as unknown and some $b$ as determined. clauseUnit is the auxiliary function that returns some $(v,b)$ precisely when a clause has exactly one unknown literal and all known literals evaluate to false, thereby forcing $v$ to $b$. Clause is the structure from RSatEncoding that packages up to three signed literal indices. The local setting is therefore a forward-chaining propagation engine that augments ordinary CNF unit propagation with XOR constraints.
proof idea
The declaration is an inductive definition whose body consists of two substantive constructors and six identity placeholders. xor_push requires that the chosen XORConstraint belongs to $H$ and that xorMissing returns the exact missing pair; clause_unit requires that the chosen Clause belongs to $φ$ and that clauseUnit returns the exact missing pair. The remaining constructors (and_one, and_zero, or_one, or_zero, not_flip, wire_prop) are identity rules that leave the state unchanged; they are introduced as syntactic placeholders for future circuit semantics.
why it matters in Recognition Science
BPStep supplies the atomic transition relation used by the downstream lemmas bp_step_monotone and bp_step_sound, which in turn feed the completeness theorems backprop_succeeds_of_unique, determined_values_correct, and geometric_isolation_enables_propagation_thm. It therefore realizes the propagation engine required by the Recognition Science treatment of SAT under XOR constraints. The definition closes the interface between the CNF/XOR encoding and the backpropagation algorithm; the gate placeholders remain open for later refinement.
scope and limits
- Does not define the reflexive-transitive closure of steps.
- Does not supply termination or progress metrics.
- Does not interpret the gate-identity constructors with concrete circuit semantics.
- Does not restrict the relation to satisfiable instances.
formal statement (Lean)
79inductive BPStep {n} (φ : CNF n) (H : XORSystem n) : BPState n → BPState n → Prop
80 | xor_push
81 {s : BPState n}
82 (X : XORConstraint n)
83 (v : Var n)
84 (b : Bool)
85 (hX : X ∈ H)
86 (hmiss : xorMissing s.assign X = some (v, b))
87 : BPStep φ H s { assign := setVar s.assign v b }
proof body
Definition body.
88 | clause_unit
89 {s : BPState n}
90 (C : Clause n)
91 (v : Var n)
92 (b : Bool)
93 (hC : C ∈ φ.clauses)
94 (hmiss : clauseUnit s.assign C = some (v, b))
95 : BPStep φ H s { assign := setVar s.assign v b }
96 -- Additional gate placeholders (to be refined with circuit semantics):
97 | and_one {s : BPState n} : BPStep φ H s s
98 | and_zero {s : BPState n} : BPStep φ H s s
99 | or_one {s : BPState n} : BPStep φ H s s
100 | or_zero {s : BPState n} : BPStep φ H s s
101 | not_flip {s : BPState n} : BPStep φ H s s
102 | wire_prop {s : BPState n} : BPStep φ H s s
103
104/-- Predicate: state is complete (all variables determined). -/