Function solve_by_symmetry_breaking 

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

Solve by breaking all symmetry first — the breaker as a front-end. Run the aux-free recursive breaker (break_all_symmetry) to collapse the symmetry to its fixpoint, then decide the reduced formula with the full arsenal (solve_comprehensive). Equisatisfiable, so the verdict is the original’s, and any returned model satisfies the original clauses (a subset of the broken set) — re-checked fail-closed. (Uses the aux-free reducer, not break_all_symmetry_complete: CDCL handles the residual cheaply, and the complete lex-leader of a large group would be far more expensive than the search it saves.)