Expand description
Fast refuter for the coupled exactly-one + parity family. An exactly-one group (an at-least-one
clause plus the full at-most-one clique over its variables) forces EXACTLY one of its selectors true,
so their XOR is 1 (odd). If the formula’s parity substructure forces that same XOR to 0 (even),
the two are inconsistent and the formula is UNSAT — the mixed obstruction neither theory sees alone.
This decides it by pure GF(2) linear algebra: recover the implied XOR system, add the equation
⊕S = 1 for an exactly-one group S, and test the augmented system for inconsistency. That is
microseconds — where the general fused route builds a whole CDCL solver with three theories (parity,
cardinality, symmetry) to reach the same verdict in milliseconds.
Soundness: the XOR equations are consequences of the formula’s gadget clauses, and any model of
the exactly-one clauses has ⊕S = 1; so if eqs ∪ {⊕S = 1} is GF(2)-inconsistent, no model satisfies
both — and the formula contains both — hence UNSAT. Conservative: fires only on a recovered
exactly-one group whose augmented parity system is inconsistent; false otherwise.
Functions§
- refute
- Refute a coupled exactly-one + parity formula.
trueiff some exactly-one group’s odd-parity requirement contradicts the formula’s XOR system. Never a false refutation.