satisfiesXOR
plain-language theorem explainer
The definition states that an assignment satisfies an XOR constraint precisely when the parity of the assigned values on the constraint's variables matches the constraint's target parity. Researchers working on SAT encodings or backpropagation soundness would cite it when checking parity conditions. The definition is a direct one-line abbreviation that unfolds the parity computation.
Claim. An assignment $a$ satisfies the XOR constraint $c$ if the parity of $a$ on the variables listed in $c$ equals the Boolean parity required by $c$.
background
An assignment for $n$ variables is a total function from variables to Boolean values. An XOR constraint is a structure holding a list of variables together with a required parity Boolean. The parityOf function computes the cumulative XOR of assignment values over a variable list, starting from false and folding with Bool.xor.
proof idea
One-line definition that directly equates the result of parityOf on the assignment and the constraint's variable list with the constraint's parity field.
why it matters
This definition supplies the basic satisfaction predicate for parity constraints. It is invoked to define satisfaction for entire XOR systems and appears inside the soundness lemma for backpropagation steps and the correctness theorem for recovering a missing variable value from a satisfying assignment. It supports the XOR encoding layer inside the SAT module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.