IndisputableMonolith.Complexity.SAT.XOR
This module defines XOR constraints and systems for SAT instances, where each constraint requires the parity of a variable subset over Fin n to equal a target bit. Researchers in SAT complexity and hybrid clause-parity reductions cite it when extending CNF with linear equations over GF(2). The module supplies inductive types for constraints and systems together with basic parity and satisfaction lemmas.
claimAn XOR constraint over $n$ variables is a subset $Ssubseteqmathrm{Fin}n$ paired with target parity $p in {0,1}$, asserting $bigoplus_{i in S} x_i = p$. An XOR system is a finite list of such constraints. The module also introduces mixed CNF-with-XOR instances and the predicates satisfiesXOR and satisfiesSystem.
background
The upstream CNF module fixes variable indices as Fin n for any given problem size. This module builds directly on that convention to encode parity equations. It defines XORConstraint to capture a subset and its required parity, XORSystem as a list of constraints, and parityOf to compute the XOR of selected bits under an assignment. Additional definitions include satisfiesXOR, satisfiesSystem, CNFWithXOR, and SatisfiableXOR, with supporting lemmas for the empty list, singletons, and cons cases.
proof idea
This is a definition module. It introduces the core types XORConstraint and XORSystem, the parityOf function, and the satisfaction predicates. Basic properties are established by direct computation for nil and singleton cases together with list induction for the cons case.
why it matters in Recognition Science
The module is imported by Backprop for partial assignments, Completeness for constructing fully determined states, GeoFamily for Morton octant masks, Isolation for size-n families, PC for mixed CNF-XOR constraints, and SmallBias for explicit small-bias families. It supplies the parity layer required for the SAT analysis inside the Recognition Science framework.
scope and limits
- Does not prove NP-completeness of XOR-SAT.
- Does not implement any solver or decision procedure.
- Does not treat weighted or real-valued relaxations.
- Does not extend beyond GF(2) linear equations.
- Does not address parameterized complexity measures.