pub fn mod_p_tseitin_expander(
n: usize,
p: u64,
seed: u64,
) -> (Vec<ModpEquation>, DimacsCnf, ExpectedVerdict)Expand description
The mod-p Tseitin obstruction on a random 3-regular expander — the parity crush carried to
every prime. Each edge carries a GF(p) flow variable; orient each edge and impose, at every
vertex, the signed divergence Σ_out − Σ_in ≡ charge (mod p). Summing all vertices telescopes the
edge variables to 0, so the system is inconsistent exactly when the total charge ≢ 0 (mod p).
We charge two vertices (total 2): inconsistent over GF(p) for every odd prime p, yet
consistent over GF(2) (2 ≡ 0) — a family the parity cut is structurally blind to, decided
instantly by Gaussian elimination over the right GF(p), and (on an expander) exponentially hard
for resolution. Returns the GF(p) system (for crate::modp), the equisatisfiable one-hot
Boolean CNF (for resolution solvers), and the GF(p) verdict.