bp_step_sound
plain-language theorem explainer
The lemma establishes that each single backpropagation step on a partial assignment for a CNF formula with XOR constraints preserves compatibility with any full satisfying assignment. Researchers formalizing SAT solvers or unit-propagation algorithms would cite it to verify that derived values remain consistent with models. The proof proceeds by case analysis on the inductive step relation, applying correctness lemmas for clause detection and XOR extraction to equate forced bits with the model before lifting compatibility.
Claim. Let $n$ be a natural number, let $φ$ be a CNF formula over $n$ variables, and let $H$ be an XOR system over the same variables. Let $s$ and $t$ be backpropagation states. If a single step relates $s$ to $t$ under $φ$ and $H$, then for every assignment $a$ that satisfies both $φ$ and $H$, compatibility of the partial assignment in $s$ with $a$ implies compatibility of the partial assignment in $t$ with $a$.
background
BPState is the structure holding a partial assignment, where each variable is either unknown (none) or fixed to a Boolean value (some b). BPStep is the inductive relation whose constructors encode the allowed propagation rules: xor_push when an XOR constraint has exactly one missing variable whose value is forced, clause_unit when a clause has exactly one unknown literal after all known literals evaluate false, and several identity rules that leave the assignment unchanged. Compatible means the partial assignment agrees with the full assignment wherever the partial is defined. The local setting is partial assignments for backpropagation over CNF plus XOR constraints, as stated in the module documentation. Upstream, clauseUnit_correct states that when clauseUnit returns (v, b) for a satisfying assignment a, then b equals a v; the analogous xorMissing_correct plays the same role for XOR constraints.
proof idea
The proof is a tactic-mode case analysis on the step hypothesis. For the xor_push case it invokes xorMissing_correct to obtain b = a v from the model satisfaction and the missing-value witness, then applies compatible_setVar. For the clause_unit case it first unfolds evalCNF to extract that the clause evaluates true under a, invokes clauseUnit_correct to equate b with a v, and again applies compatible_setVar. All remaining constructors (and_one, and_zero, or_one, or_zero, not_flip, wire_prop) leave the assignment unchanged, so compatibility is immediate by assumption.
why it matters
This lemma supplies the inductive step for soundness of the entire backpropagation process in the SAT module. It ensures that every derived partial assignment remains faithful to any model of the original formula and XOR system, closing the local correctness argument before global termination or completeness results are considered. In the Recognition Science framework it supports the complexity analysis by guaranteeing that constraint propagation respects the underlying algebraic cost structure without introducing spurious assignments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.