pub fn random_kxor(
k: usize,
n: usize,
m: usize,
seed: u64,
) -> (Vec<XorEquation>, DimacsCnf)Expand description
A guaranteed-unsatisfiable random k-XOR (parity) system over n variables: at least m
equations of k distinct variables, all consistent with a planted assignment p except one whose
right-hand side is flipped. Generalizes parity_unsat (the k = 3 case).
The flip alone does not force inconsistency — it does so only once the flipped row lies in the
span of the others, which a naive “flip the last equation” does not guarantee near m ≈ n (it
silently yields satisfiable instances). So we build the consistent rows until the coefficient
matrix reaches its maximum achievable GF(2) rank (n for odd k; n − 1 for even k, whose
even-weight rows can never span the all-ones functional) and at least m rows total, then append
one more equation with a flipped right-hand side. At maximal rank that final row is redundant, so the
system’s solution set — {p} for odd k, {p, p̄} for even k — is pinned, and every pinned
solution violates the flipped row: the system is inconsistent by construction, for any seed.
Full-rank k-XOR above the XOR-SAT threshold is also exponentially hard for resolution
(Ben-Sasson–Wigderson 2001) — hence for every CDCL solver — yet linear for Gaussian elimination over
GF(2). Each equation expands to 2^{k-1} width-k clauses, so keep k modest. m is a floor on the
equation count (full rank may need a few more). Returns the XOR equations and the equisatisfiable CNF.