compatible_setVar
plain-language theorem explainer
Updating a partial assignment by fixing one variable to its value under a compatible total assignment preserves compatibility. Researchers proving soundness of backpropagation steps in SAT solvers augmented with XOR constraints cite this preservation property. The argument splits on whether the queried variable matches the updated one and reduces directly via the setVar_same and setVar_ne lemmas.
Claim. Let $n$ be a natural number, let $a$ be a total assignment (a function from variables to Booleans), and let $v$ be a variable. If a partial assignment $σ$ (a function from variables to optional Booleans) is compatible with $a$, then the partial assignment obtained by setting the entry for $v$ to $a(v)$ remains compatible with $a$.
background
A PartialAssignment n is a map from each variable to either none (undetermined) or some Boolean value. Compatibility of $σ$ with a total assignment $a$ holds precisely when, for every variable, either $σ$ has not yet determined a value or the determined value equals $a$ at that variable. The setVar operation replaces the entry for a chosen variable with a fixed Boolean while leaving all other entries unchanged.
proof idea
The proof performs case analysis on the queried variable $w$ relative to the updated variable $v$. When $w = v$, setVar_same immediately yields the required some (a v) entry. When $w ≠ v$, setVar_ne rewrites the updated map back to the original $σ$ at $w$, so the compatibility hypothesis applies directly.
why it matters
This lemma is invoked by bp_step_sound to establish that each propagation step preserves compatibility with any satisfying assignment. It therefore supplies a key semantic invariant for the backpropagation procedure over CNF formulas with XOR constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.