compatible_setVar
plain-language theorem explainer
Updating a partial assignment by fixing one variable to its value under a total assignment preserves compatibility between the partial and total assignments. Backpropagation soundness proofs in SAT solvers cite this result when showing that propagation steps maintain agreement with models. The proof uses case distinction on the variable being updated and applies the setVar_same and setVar_ne lemmas to reduce to the original compatibility assumption.
Claim. If a partial assignment $σ$ over $n$ variables is compatible with a total assignment $a$, then for any variable $v$ the updated partial assignment obtained by setting the entry for $v$ to $a(v)$ remains compatible with $a$.
background
A PartialAssignment n is a map from variables (Fin n) to Option Bool, with none marking an undetermined entry and some b marking a fixed Boolean value. Compatibility of σ with a total assignment a (Fin n → Bool) means that for every variable the partial entry is either none or exactly matches a at that variable. The setVar operation replaces the entry at a chosen variable v with a supplied Boolean while leaving all other entries unchanged.
proof idea
The proof performs case analysis on whether the queried variable equals the updated variable. When they coincide it substitutes and invokes setVar_same to obtain the left disjunct of compatibility. When they differ it rewrites with setVar_ne and applies the original compatibility hypothesis directly.
why it matters
This lemma is invoked inside bp_step_sound to establish that each backpropagation step preserves compatibility with any satisfying assignment of the CNF and XOR system. It therefore contributes to the semantic correctness argument for the entire propagation procedure on SAT instances with XOR constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.