setVar
plain-language theorem explainer
The setVar operation updates a partial assignment over n variables by fixing one variable index to a chosen Boolean value. Researchers constructing backpropagation steps for SAT instances with XOR constraints cite this when building state transitions. The definition implements the update as a direct pointwise conditional on the variable index.
Claim. Let $n$ be a natural number, let $σ : Var(n) → Option(Bool)$ be a partial assignment, let $v : Var(n)$ be a variable index, and let $b : Bool$. Then setVar$(σ, v, b)$ is the partial assignment $w ↦$ some$(b)$ if $w = v$, and $σ(w)$ otherwise.
background
PartialAssignment n is the type of maps from variable indices to Option Bool, where none denotes an undetermined value and some b denotes a fixed Boolean. Var n is the type Fin n of indices for an n-variable problem. The module treats these partial assignments as the state for backpropagation over CNF formulas augmented by XOR systems, with none meaning unknown and some b meaning determined.
proof idea
The definition is supplied directly as a lambda that returns some b on the target variable and delegates to the input assignment elsewhere. No lemmas are invoked; the body is the complete implementation.
why it matters
setVar supplies the atomic update used to define the BPStep inductive relation and to prove its monotonicity and soundness lemmas. It appears in the hypotheses of compatible_setVar, setVar_same, and setVar_ne, which in turn support the backpropagation soundness argument. Within the Recognition framework this operation models constraint propagation steps that sit inside the broader analysis of computational complexity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.