Skip to main content

affine_p_canonicalize

Function affine_p_canonicalize 

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

The GF(p) canonical RREF break (elimination). The one-hot analogue of crate::affine::affine_canonicalize: recover the mod-p system and solve its space, then physically eliminate the determined one-hot groups rather than merely injecting their consequences. A forced group’s bits become constants; a linked group’s bits alias to its representative’s, value-permuted (b(g,v) = b(rep, σ(v)) with σ(v) = (v−d)·c⁻¹). The result is an equisatisfiable formula over the surviving (free/representative) groups, with AffinePCanonical::lift to recover the eliminated bits. An inconsistent core AffinePCanon::Refuteds; a composite modulus is left to affine_m_forced.