pub fn emit_xor_drat(
equations: &[XorEquation],
refutation: &[usize],
) -> Option<Vec<Vec<Lit>>>Expand description
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.