pub fn break_all_symmetry_complete(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> (Vec<Vec<Lit>>, usize)Expand description
Complete symmetry breaking — the breaker driven all the way to a single representative per orbit.
Detect the full variable-symmetry group and add the COMPLETE lex-leader (one a ≤_lex a∘g per group
element, via the standard lex-chain auxiliaries), which admits exactly one model per symmetry orbit
when the group is enumerable. Returns the strengthened clauses and the new variable count (originals +
auxiliaries). Sound (equisatisfiable with the input); complete for groups up to the enumeration cap, and
a sound partial break (generators ∪ coset representatives) for larger ones. Unlike break_all_symmetry
(aux-free, complete only for fully-symmetric orbits), this leaves no residual orbit symmetry.