setVar
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not check consistency of the new assignment against any clause or XOR constraint.
- Does not propagate implications to other variables.
- Does not evaluate the full CNF or XOR system.
- Does not alter the domain size n.
Lean usage
lemma example {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : setVar σ v b v = some b := setVar_same σ v bformal statement (Lean)
17def setVar {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : PartialAssignment n :=
proof body
Definition body.
18 fun w => if w = v then some b else σ w
19