pub fn extract_xor(num_vars: usize, clauses: &[Vec<Lit>]) -> Vec<XorEquation>Expand description
Recover the XOR (parity) constraints latent in a CNF: a constraint x₁⊕…⊕x_k = b is encoded by
exactly the 2^(k-1) clauses over {x₁,…,x_k} whose negated-literal count has one fixed parity.
We group clauses by their variable set and emit an XorEquation for each group that is exactly
such a gadget. Sound: every emitted equation is logically equivalent to a clause group present in
the formula, so a refutation of the extracted (sub)system implies the formula is UNSAT.