Module sym_break 

Complete lex-leader symmetry breaking, driven by the Schreier–Sims backend.

Per-generator symmetry breaking keeps a superset of the canonical representatives. With the whole group in hand — enumerated from a BSGS (crate::permgroup) — we add the COMPLETE lex-leader predicate a ≤_lex a∘g for every g ∈ G, which keeps EXACTLY the lexicographically-least model of each orbit: the maximal sound symmetry break. Satisfiability is preserved (every orbit keeps one representative), and the number of surviving models equals the number of orbits of models.

This is feasible when |G| is small/moderate — the BSGS reports the order, so the caller gates on it before enumerating. Huge-symmetry families (PHP at scale, |Aut| = n!·(n−1)!) are left to the dedicated polynomial specialists; complete lex-leader is for the moderate-symmetry instances those do not target. Scope: variable permutations (phase-free automorphisms — the symmetry of the covering/colouring families), acting on assignments by (a∘g)[j] = a[g[j]].

Functions

affine_lex_leader_sbp

The lex-leader SBP for affine maps α: x ↦ Ax ⊕ b over GF(2) — the machinery that breaks the affine parity symmetries a variable/literal permutation SBP (lex_leader_sbp) structurally cannot express (an image bit is an XOR of several variables, not one literal). Each maps[k] is a per-output spec: maps[k][j] = (A_j, b_j) with α(x)[j] = ⊕_{i∈A_j} x_i ⊕ b_j. Each non-identity output is Tseitin-encoded as a fresh variable, then the standard prefix-equality chain [encode_lex_le] enforces x ≤_lex α(x). Satisfiability-preserving for any model-set affine symmetry (the lex-least model of each orbit survives). Returns the extra clauses and the new total variable count (aux appended above num_vars).

conditional_symmetry_generators

Conditional (local) symmetry — the symmetry of the RESIDUAL formula after a partial assignment. A formula can be globally asymmetric yet its residual F|ρ symmetric: symmetries that emerge only down a branch, invisible to a global automorphism search. Returns the residual’s literal-symmetry generators (image-literal form). This is a different symmetry source — the basis for local symmetry breaking during search, where each decision can unlock fresh symmetry to exploit.

count_models_modulo_symmetry

The number of essentially-distinct solutions — models counted up to the formula’s symmetry: the orbit count of the solution set (#SAT modulo G). The complete lex-leader keeps exactly one model per orbit, so counting the symmetry-broken formula’s models is the orbit count. None if the symmetry group is too large to enumerate for the complete break. The counting face of symmetry breaking — and, by Burnside, (1/|G|)·Σ_σ #{models fixed by σ}.

hierarchical_break

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.

is_lex_leader

Is a the lexicographic leader of its orbit — a ≤_lex a∘g for every g? The semantic canonical test; the CNF predicate lex_leader_sbp accepts exactly these assignments.

is_lex_leader_lit

is_lex_leader over literal symmetries: aˢ[j] is the value of the image literal img[j] under a (a phase flip negates the compared bit).

lex_leader_sbp

The lex-leader symmetry-breaking predicate as CNF: for every non-identity g ∈ group, clauses asserting a ≤_lex a∘g. Returns the extra clauses plus the new total variable count (prefix-equality aux variables are appended above num_vars). It is satisfiability-preserving for any set of automorphisms (the lex-least model of each orbit always survives). Pass the whole group for the COMPLETE break (exactly one model per orbit), or just a generating set for a sound POLYNOMIAL PARTIAL break that scales to arbitrarily large groups — both keep at least one representative per orbit.

lex_leader_sbp_lit

The lex-leader SBP over literal symmetries (group[k][j] = the image literal of variable j), which breaks variable and value/phase symmetry alike. As with lex_leader_sbp, pass the whole group for the complete break or a generating set for the polynomial partial break.

literal_automorphism_generators

The literal-permutation automorphism GENERATORS — variable AND value/phase symmetry — as image-literal vectors (imgⱼ = σ(+xⱼ)). Unlike variable_automorphism_generators, phase flips are kept, so this captures the symmetry of formulas invariant under negating variables. Empty if none.

literal_automorphism_group

The full literal-automorphism group (variable + value symmetry) enumerated via the Schreier–Sims backend on the 2·num_vars literal points, for the complete break. None if |G| > cap (use the generators for the polynomial partial break instead).

litsym_from_points

A permutation of the 2·num_vars literal points back to a literal symmetry (img[j] from where +xⱼ goes). Inverse of litsym_to_points.

litsym_to_points

A literal symmetry (img[j] = image literal of variable j) as a permutation of the 2·num_vars literal points — for the Schreier–Sims backend (order, enumeration). Negation is respected.

variable_automorphism_generators

The variable-permutation automorphism GENERATORS of a CNF (phase-free symmetries), without enumerating the group — fast, no size cap. None if a detected symmetry flips a phase (a value symmetry this variable scheme does not cover). An empty vector means no non-trivial symmetry.

variable_automorphism_group

The variable-permutation automorphism group of a CNF, fully enumerated via the Schreier–Sims backend (for complete symmetry breaking). None if a generator flips a phase, or |G| > cap (then the caller should use per-generator partial breaking on variable_automorphism_generators instead, which scales to arbitrarily large groups).