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.