Skip to main content

parity_unsat

Function parity_unsat 

Source
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).