xorMissing
plain-language theorem explainer
xorMissing returns the single unknown variable in an XOR constraint together with the Boolean value that satisfies the target parity once all other variables are known under the partial assignment. Researchers building SAT solvers or backpropagation procedures over mixed CNF-XOR systems would cite the definition when implementing unit propagation for parity constraints. The body filters the variable list for unknowns and, on a singleton, folds the known assignments to compute the required parity correction.
Claim. Let $n$ be a natural number, let $σ$ map each variable in $Fin n$ to an optional Boolean, and let $X$ be an XOR constraint consisting of a list of variables together with a target parity $p$. The function returns $some(v,b)$ precisely when exactly one variable $v$ is unmapped by $σ$, where $b$ is chosen so that the XOR of the known values with $b$ equals $p$; otherwise it returns $none$.
background
PartialAssignment $n$ is the type $Var n → Option Bool$, where $none$ marks an undetermined value and $some b$ records a fixed Boolean. An XORConstraint $n$ is the structure whose fields are a list of variables and a Boolean parity that their assignments must satisfy under XOR. The module develops single-step backpropagation over CNF formulas that may contain both ordinary clauses and XOR constraints, using partial assignments to propagate forced values. Upstream, the definition of XORConstraint supplies the vars and parity fields, while Var is simply $Fin n$.
proof idea
The definition first builds the sublist of variables in $X.vars$ whose image under $σ$ is none. When that sublist has length one it selects the variable at index zero and folds over the full variable list, accumulating the XOR of every known Boolean value (defaulting missing entries to false). The required value for the unknown variable is then the XOR of the constraint parity with the accumulated known parity.
why it matters
The definition supplies the propagation rule invoked inside the inductive constructor xor_push of BPStep and is the key lemma in both bp_step_sound and xorMissing_correct. The latter theorem records that the returned pair matches the value any satisfying assignment must assign to that variable. In the Recognition Science framework it supports the complexity analysis of constraint systems that appear when physical quantities are discretized onto the φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.