pub fn affine_refutation_drat(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<Vec<Vec<Lit>>>Expand description
The clausal DRAT certificate for an affine refutation, or None if the formula’s linear core is
not inconsistent (or num_vars exceeds the u64 mask, or the resolution expansion overruns its
budget). Recovers the XOR system, finds the GF(2) linear dependency that sums to 0 = 1
(crate::xorsat::solve), and compiles it to RUP resolvent lemmas through the crate::xor_drat
bridge — the same path Route::Parity uses, so it is drat-trim-checkable against the original CNF.