Skip to main content

affine_m_canonicalize

Function affine_m_canonicalize 

Source
pub fn affine_m_canonicalize(
    num_bool_vars: usize,
    clauses: &[Vec<Lit>],
) -> AffinePCanon
Expand description

The composite-ring canonical elimination. The ℤ/m analogue of affine_p_canonicalize and the eliminate twin of [prime_power_forced]: over a non-prime modulus, recover the mod-m system, take its [composite_break_structure], and physically eliminate the determined one-hot structure rather than merely injecting it. A forced group (x_g pinned to a single value) becomes constants; a partially forced group (x_g confined to a coset v ≡ res (mod modu), 1 < modu < m) keeps only its on-coset bits, the rest pinned false; a linked group’s bits alias its representative’s, value-permuted (b(g,v) = b(rep, σ(v)), σ(v) = (v−d)·c⁻¹ mod m). The result is equisatisfiable over the surviving bits, with AffinePCanonical::lift to recover the rest. An inconsistent component AffinePCanon::Refuteds; a prime modulus is left to affine_p_canonicalize.