pub fn hierarchical_break(
num_vars: usize,
clauses: &[Vec<Lit>],
) -> Option<(Vec<Vec<Lit>>, usize)>Expand description
Hierarchical (block-wise) symmetry breaking. For an imprimitive symmetry — a grid like PHP or
graph colouring — the minimal block system splits the variables into equal blocks (e.g. the rows). The
adjacent block-swaps (inter-block) and the uniform adjacent within-block swaps (intra-block)
are STRUCTURED generators; each is verified to actually lie in the group (Bsgs::contains), then their
lex-leader is the “sorted blocks, sorted within” break — a POLYNOMIAL set of O(blocks + block-size)
constraints that breaks the wreath/product symmetry for which the complete enumeration would need |G|
(exponential) clauses. Sound (it only uses verified group elements). None if the group is primitive,
has no phase-free symmetry, or no structured generator lies in it. Scope: variable (phase-free) grids.