Skip to main content

mod_m_tseitin_expander

Function mod_m_tseitin_expander 

Source
pub fn mod_m_tseitin_expander(
    n: usize,
    m: u64,
    seed: u64,
) -> (Vec<ModpEquation>, DimacsCnf, ExpectedVerdict)
Expand description

The composite-modulus sibling of mod_p_tseitin_expander: the same total-charge-2 divergence obstruction over ℤ/m for a squarefree composite m (e.g. m = 6), with a mixed-radix one-hot Boolean encoding (m values per edge). By CRT ℤ/m ≅ ∏ GF(pᵢ), so the system is inconsistent over ℤ/m exactly when it is inconsistent over some prime factor — total charge 2 ≢ 0 (mod m) for any m ≥ 3 that does not divide 2 — and crate::modm::solve decides it through that factor with a solver-free re-checkable certificate (crate::modm::is_refutation). This drives the ring route (ℤ/m Gaussian via CRT), not the prime-field route, on a CNF that resolution still walls on.