pub fn parity_unsat(
n: usize,
m: usize,
seed: u64,
) -> (Vec<XorEquation>, DimacsCnf)Expand description
A guaranteed-unsatisfiable random 3-XOR (parity) system — the k = 3 case of random_kxor:
at least m 3-XOR equations over n variables, all consistent with a planted assignment except one
flipped row, built up to maximal GF(2) rank so the inconsistency holds for any seed (see
random_kxor for why the naive single flip does not suffice). Full-rank 3-XOR above the XOR-SAT
threshold is exponentially hard for resolution (Ben-Sasson–Wigderson 2001), hence for every CDCL
solver — yet linear for Gaussian elimination over GF(2). Returns the XOR equations (for
crate::xorsat) and the equisatisfiable CNF (for a resolution solver).