Function cardinality_symmetry_break 

pub fn cardinality_symmetry_break(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Vec<Vec<Lit>>

Break the joint cardinality/parity symmetry: union the joint swaps into interchangeable components (a component is fully symmetric — the group generated by its transpositions is S, every element an automorphism), then order each component’s variables into a descending chain with vᵢ ≥ vᵢ₊₁ clauses (vᵢ ∨ ¬vᵢ₊₁). A lex-leader: equisatisfiable (every orbit keeps its ordered representative), so it shrinks the fused search without changing the verdict. Returns the extra clauses (empty if no joint symmetry).