Module xor_engine 

DPLL(XOR) — the live GF(2) reasoning engine.

A system of XOR (parity) constraints x_{i1} ⊕ … ⊕ x_{ik} = b is a linear system over GF(2). Plain CDCL refutes it only through resolution, which is exponential on parity (Tseitin/par families); Gaussian elimination decides it in polynomial time. This engine carries that linear reasoning into the search: given the solver’s current partial assignment it derives every XOR-forced literal — and detects contradiction — by Gaussian elimination over the unassigned variables, so the solver never has to rediscover linear consequences by resolution.

Soundness is the whole game. Every clause this engine hands back to CDCL is the gadget clause of a derived equation E* = Σ_{i∈P} E_i (a GF(2) sum of recovered equations, tracked by the provenance set P). Each E_i is a logical consequence of the formula (a full XOR gadget’s clauses imply its equation), so E* is too, and so is the single gadget clause we emit — which is exactly unit (one unassigned literal) when E* forces a variable, or fully falsified when E* is violated. The engine therefore can never make the solver unsound; it can only make it faster.

This module is the correctness-validated core (an exhaustive brute-force oracle checks that the derived forced-literals/conflicts are precisely the GF(2) consequences, and that every emitted clause is implied and correctly unit/falsified). The incremental watched-matrix that makes it cheap per call is layered on top of this oracle.

Structs

IncXor

Incremental GF(2) engine — the fast DPLL(XOR) core.

XorEngine

A GF(2) constraint system with Gaussian reasoning under a partial assignment.

Enums

XorStep

The result of consulting the engine at a Boolean fixpoint.