Function affine_p_forced 

pub fn affine_p_forced(
    num_bool_vars: usize,
    clauses: &[Vec<Lit>],
) -> AffinePForced

The GF(p) SAT-side break. Recover the one-hot mod-p system (crate::modp::recover_from_cnf) and solve its solution space (crate::modp::solve_space), whose kernel is the affine translation symmetry. Two structures fall out, the mod-p analogues of crate::affine::affine_reduce’s forced units and equivalence classes:

• Forced — a GF(p) variable the kernel never moves is pinned to a single value v; lift that through the one-hot encoding (the group’s bit for v true, the rest false) to Boolean units.
• Linked — variables whose kernel columns are scalar-proportional satisfy x_g = c·x_rep + d in every solution. That lifts to value-permuted bit-equivalences b(g,v) ↔ b(rep, (v−d)·c⁻¹) — the genuinely GF(p) shear-links no monomial break can see, the value permutation a clause equivalence cannot express on its own.

Every emitted clause is GF(p)-entailed by the formula (sound to conjoin) and new. An inconsistent core instead AffinePForced::Refuteds (certified).