pub fn affine_p_canonicalize(
num_bool_vars: usize,
clauses: &[Vec<Lit>],
) -> AffinePCanonExpand 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.