compatible_setVar
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the updated partial assignment satisfies any clause of the original formula.
- Does not address the case in which the original partial assignment already conflicts with the total assignment.
- Does not extend the preservation property to simultaneous updates of multiple variables.
Lean usage
lemma use_compatible_setVar {n} (σ : PartialAssignment n) (a : Assignment n) (v : Var n) (h : compatible σ a) : compatible (setVar σ v (a v)) a := compatible_setVar σ a v hformal statement (Lean)
118lemma compatible_setVar {n} (σ : PartialAssignment n) (a : Assignment n) (v : Var n)
119 (hcompat : compatible σ a) :
120 compatible (setVar σ v (a v)) a := by
proof body
Term-mode proof.
121 intro w
122 by_cases hwv : w = v
123 · subst hwv
124 left
125 simp [setVar_same]
126 · rw [setVar_ne σ v w (a v) hwv]
127 exact hcompat w
128
129/-!
130## Semantic Correctness for XOR Propagation
131
132The xorMissing function produces the correct value for a satisfying assignment.
133This is now a **proved theorem**, not an axiom.
134-/
135
136-- Helper lemmas for xorMissing_correct proof