Function solve_with_declared_symmetry 

pub fn solve_with_declared_symmetry(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    declared: &[Perm],
) -> Solved

The full arsenal with caller-DECLARED symmetry. The modeler often knows symmetries the automatic detector cannot afford to find (geometric, semantic, or simply large). This entry point accepts declared variable-permutation generators, verifies each is a genuine symmetry ([is_declared_symmetry] — never trusting a declaration blindly, so an incorrect one is silently dropped), unions the survivors with the auto-detected symmetry, and breaks the combined group with the lex-leader (complete by enumeration when the group is small, partial over the generators otherwise). Sound: only verified, model-set- preserving permutations enter the break; a SAT model is re-checked, and on any anomaly it falls back to the authoritative solve_comprehensive. With no declared and no detected symmetry it simply is solve_comprehensive.