Skip to main content

cardinality_symmetry_generators

Function cardinality_symmetry_generators 

Source
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_m inside each orbit;
  • block — whole joint orbits mapped to each other across the seams ((0 2)(1 3) when the individual 0↔2, 1↔3 are seams): automorphisms of the quotient, the family S_k permuting the k blocks.

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.