satisfiesSystem
plain-language theorem explainer
An assignment satisfies an XOR system precisely when it meets the parity requirement of every constraint in the list. Researchers formalizing hybrid SAT solvers with parity clauses cite the definition when proving soundness of belief-propagation updates or completeness of value determination. The definition is a direct universal quantification that delegates each check to the single-constraint predicate.
Claim. Let $a$ be a total Boolean assignment to $n$ variables and let $H$ be a finite list of XOR constraints. Then $a$ satisfies $H$ if and only if, for every constraint $c$ in $H$, the parity of the variables selected by $c$ under $a$ equals the target parity recorded in $c$.
background
An XOR constraint records a subset of variables together with a required parity bit. An XOR system is the corresponding finite list of such constraints. An assignment is a total map from the $n$ variables to Boolean values. The single-constraint predicate checks whether the parity computed on the selected variables matches the recorded target. The system predicate simply lifts that check to every member of the list. This construction augments ordinary CNF satisfiability with linear equations over GF(2).
proof idea
The definition is a one-line abbreviation consisting of a universal quantifier over the list $H$ that applies the single-constraint satisfaction predicate to each element.
why it matters
The predicate is used to define consistent states and unique solutions for mixed CNF-XOR formulas. It is invoked inside the soundness lemma for a single belief-propagation step and inside the completeness theorem that recovers a satisfying assignment from determined values. It therefore supplies the semantic bridge between partial assignments maintained by the solver and total models of the combined constraint set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.