pub fn lex_leader_sbp(num_vars: usize, group: &[Perm]) -> (Vec<Vec<Lit>>, usize)Expand description
The lex-leader symmetry-breaking predicate as CNF: for every non-identity g ∈ group, clauses
asserting a ≤_lex a∘g. Returns the extra clauses plus the new total variable count (prefix-equality
aux variables are appended above num_vars). It is satisfiability-preserving for any set of
automorphisms (the lex-least model of each orbit always survives). Pass the whole group for the
COMPLETE break (exactly one model per orbit), or just a generating set for a sound POLYNOMIAL
PARTIAL break that scales to arbitrarily large groups — both keep at least one representative per orbit.