pub fn affine_m_forced(
num_bool_vars: usize,
clauses: &[Vec<Lit>],
) -> AffinePForcedExpand description
The composite ℤ/m SAT-side break (squarefree m), the full mod-m analogue of
affine_p_forced via CRT (ℤ/m ≅ ∏ GF(pᵢ)). Solve the system over each prime field, then for each
variable combine the per-prime structure:
- Forced / partially forced — where the kernel pins
x_gmod a setSof primes,x_gis congruent to one residue mod∏S; forbid every one-hot value off that residue (a single allowed value whenSis all primes — the fully-forced units). - Linked — variables free mod every prime whose kernel columns are scalar-proportional mod each
prime are linked over
ℤ/mbyx_g = c·x_rep + dwithc = CRT(cᵢ),d = CRT(dᵢ); lift to value-permuted bit-equivalencesb(g,v) ↔ b(rep, (v−d)·c⁻¹ mod m).
Every emitted clause is ℤ/m-entailed and new; an inconsistent prime field AffinePForced::Refuteds.
A prime modulus defers to affine_p_forced; a non-squarefree m (prime-power Smith case) is untouched.