Skip to main content

mod_p_tseitin_expander

Function mod_p_tseitin_expander 

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