Skip to main content

affine_m_forced

Function affine_m_forced 

Source
pub fn affine_m_forced(
    num_bool_vars: usize,
    clauses: &[Vec<Lit>],
) -> AffinePForced
Expand 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_g mod a set S of primes, x_g is congruent to one residue mod ∏S; forbid every one-hot value off that residue (a single allowed value when S is all primes — the fully-forced units).
  • Linked — variables free mod every prime whose kernel columns are scalar-proportional mod each prime are linked over ℤ/m by x_g = c·x_rep + d with c = CRT(cᵢ), d = CRT(dᵢ); lift to value-permuted bit-equivalences b(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.