pub fn cardinality_symmetry_generators(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Vec<Vec<usize>>Expand description
The generators of the joint parity/cardinality symmetry, UP THE WREATH CHAIN. Two levels:
- within-orbit — the joint swaps (interchangeable variables), the class
S_minside each orbit; - block — whole joint orbits mapped to each other across the seams (
(0 2)(1 3)when the individual0↔2,1↔3are seams): automorphisms of the quotient, the familyS_kpermuting thekblocks.
Together these generate the wreath product S_m ≀ S_k. Feed to crate::sym_break::lex_leader_sbp to
break class and family at once — pulling the symmetry apart on the seams, not just within them. Block
pairs are tested under the sorted correspondence (a sound heuristic — only genuine automorphisms are
emitted), budget-bounded.