Module xorsat 

XOR-SAT via Gaussian elimination over GF(2) — the parity analog of the pigeonhole/matching supercrush.

A system of parity (XOR) constraints — x₁ ⊕ x₃ ⊕ x₇ = 1, etc. — is the canonical resolution-hard problem: Tseitin formulas over expander graphs need exponentially long resolution refutations, so CDCL solvers (ours and Z3 alike) blow up on the CNF encoding. But the underlying question is just a linear system over GF(2), decided in polynomial time by Gaussian elimination — and certified: an inconsistent system yields a subset of equations whose XOR is 0 = 1 (a re-checkable linear-dependency refutation), and a consistent one yields a satisfying assignment. Parity systems are everywhere — cryptanalysis, error-correcting codes, checksum logic — so this is a broad class we decide instantly where SAT/Z3 cannot.

Structs

XorEquation

A parity equation: the XOR of the variables in vars equals rhs. (Repeated variables cancel, per GF(2).)

Enums

XorOutcome

The outcome of solving an XOR system.

Functions

is_refutation

Re-check a refutation: the XOR of the chosen equations is 0 = 1 — their variables all cancel while their right-hand sides sum to 1. A solver-free certificate of unsatisfiability.

refute_via_parity

Recognize the XOR (parity) gadgets inside a CNF ProofExpr and refute via Gaussian elimination — the GF(2) shadow, as a fast-path for crate::sat::prove_unsat. A parity constraint x_{a} ⊕ … ⊕ x_{z} = r over k variables is encoded in CNF as exactly the 2^{k-1} clauses that forbid the wrong-parity assignments; we group clauses by their variable set, and whenever a group is precisely such a full wrong-parity bundle we recover its XorEquation.

satisfies

Re-check a satisfying assignment: every equation’s variable-XOR equals its rhs.

solve

Solve a parity system over 0..num_vars by Gauss–Jordan elimination over GF(2). Returns a satisfying assignment or a certified 0 = 1 refutation. O(eq · vars · (eq+vars)/64).