Module xor_drat 

The CNF→GF(2) bridge: compile a Gaussian (XOR linear-dependency) refutation into a strict DRAT proof that an external checker (drat-trim) accepts.

Our parity route refutes Tseitin/XOR formulas by linear algebra: it finds a set S of recovered XOR equations whose GF(2) sum telescopes to 0 = 1 (crate::xorsat::solve → Unsat(S)). That certificate is sound and re-checkable algebraically — but it is not the Boolean clausal proof the competition toolchain consumes. This module closes that gap.

The construction (why each emitted line is RUP). Every equation in S is encoded in the CNF by its full parity gadget (the 2^{k-1} clauses forbidding wrong-parity assignments). The conjunction of the gadgets of S is unsatisfiable (their linear combination is 0 = 1), so the empty clause is derivable from them by resolution. We produce that derivation by Davis–Putnam variable elimination over the support, in min-degree order, emitting each resolvent as a proof line. A resolvent of two clauses already in the formula is RUP (reverse-unit-propagation) against that formula, and we only ever grow the formula — so every line checks, and the final line is the empty clause. The proof is polynomial when the elimination keeps clauses narrow (bounded cut-/tree-width); it can blow up on high-expansion instances, which is the honest limit of the resolution route (the polynomial extension-variable construction is the next rung).

Soundness is independent of how the equations were recovered: the gadget clauses we resolve over are entailed by the CNF, and the emitted proof is checked by drat-trim against the original formula, so a faulty recovery cannot produce an accepted proof.

Functions

emit_drat_over_support

Resolution-refute the sub-CNF confined to the support variables — the convention-agnostic bridge. The emitted clauses are resolvents of real CNF clauses, so each is RUP against the original formula by construction and a drat-trim check holds. None if that sub-CNF is not UNSAT (so the caller’s algebraic verdict could not be reproduced clausally — a fail-closed signal).

emit_modp_drat

The CNF→GF(p) bridge: compile a modular (mod-p / counting) UNSAT verdict into a strict DRAT proof. We recover the one-hot modular system from clauses, solve it over the prime field, and — on UNSAT — resolution-refute the sub-CNF confined to the one-hot bits of the involved groups. That sub-CNF (the forbidden-tuple gadgets of the combination’s equations together with their groups’ at-least-one/at-most-one clauses) is unsatisfiable, so DP elimination over those Boolean variables yields the empty clause, every line RUP against the original CNF. None if the formula is not a recoverable mod-p encoding or its modular system is satisfiable.

emit_xor_drat

Compile the GF(2) linear-dependency refutation refutation (equation indices whose XOR is 0=1, from crate::xorsat::solve) into a DRAT proof: the ordered resolvent clauses, ending in the empty clause. Pair these with the original CNF for crate::rup::check_refutation or drat-trim.

gadget_clauses

The full parity gadget of eq: one clause per wrong-parity assignment of its variables. These are exactly the CNF clauses a Tseitin/XOR encoding carries for the constraint.