Skip to main content

forced_values_squarefree

Function forced_values_squarefree 

Source
pub fn forced_values_squarefree(
    equations: &[ModpEquation],
    num_vars: usize,
    m: u64,
) -> Option<ForcedM>
Expand description

Which variables a squarefree ℤ/m system forces to a single value, by CRT of the GF(pᵢ) solution spaces (ℤ/m ≅ ∏ GF(pᵢ)): a variable is forced mod m iff it is forced mod every prime factor (crate::modp::solve_space — its kernel never moves it), and the value is the CRT of those residues. None if m is not squarefree (the prime-power case needs Smith normal form, not handled here). This is the substrate of the composite affine SAT-side break.