Skip to main content

break_all_symmetry_complete

Function break_all_symmetry_complete 

Source
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.