Module solve 

Structure-detecting solve front-end — the auto-dispatcher that puts our whole arsenal behind a single entry point.

An opaque CNF is offered, in cost order, to a battery of CHEAP (O(clauses)) structure recognizers — each polynomial on structure that costs plain CDCL/resolution exponentially, and each FAIL-CLOSED: it claims a verdict only with a re-checked certificate (a Hall witness, a cutting-plane derivation, a GF(2) refutation, a covering-measure collapse, or — the complete deciders — a 2-SAT/Horn model). Anything no recognizer fires on is decided by the authoritative CDCL core. Every recognizer is cheap to apply AND to reject, so the dispatcher is never slower than the plain solver — only faster when structure is present.

Routes, in order:

1. 2-SAT (twosat) — every clause ≤ 2 literals: linear, decides SAT (with model) or UNSAT.
2. Horn (hornsat) — every clause ≤ 1 positive literal: linear least-model / refutation.
3. LLL (lll) — satisfiability from sparsity: when every clause shares variables with few others (e·2^{-w}·(d+1) ≤ 1), a model is guaranteed and constructed by Moser–Tardos. The SAT-side specialist, dual to the UNSAT recognizers below.
4. Pigeonhole / Hall (pigeonhole::decide_pigeonhole_unsat) — bipartite-matching infeasibility: crushes pigeonhole (PHP) instances of any size in microseconds.
5. Cutting planes (pseudo_boolean::refute_clausal) — cardinality refutation.
6. Parity / GF(2) (xorsat::refute_via_parity) — XOR/Tseitin linear systems.
7. Covering collapse (lyapunov::auto_collapse) — auto-discovers the covering symmetry (pigeonhole, clique-colouring, …) or parity collapse with a Lyapunov-certified artifact.
8. CDCL — the authoritative fallback (model on SAT, RUP proof on UNSAT).

Structs

Solved

A decided instance.

SymmetricCount

The solution set described up to symmetry: one representative per orbit, plus the exact total.

SymmetryProfile

The structural profile of a formula’s variable-symmetry group — |Aut|, the orbit/rank/transitivity ladder, primitivity, and block structure. The data a surfacing layer (e.g. a Studio panel) needs to explain why an instance is symmetric.

Enums

Answer

The verdict; a model on SAT, with any UNSAT certificate carried in Solved::proof.

EquivVerdict

The verdict of a symmetry-reduced equivalence check.

Route

Which engine decided the instance.

Functions

almost_symmetry_pairs

The almost-symmetries (variable transpositions) of a CNF: pairs (a,b) whose swap preserves all but at most max_broken clauses. Returns each pair with the broken images σ(B) = { swap(c) : swap(c) ∉ F } — the clauses that must hold for the swap to map a model to a model, i.e. the guard. An empty image set is a true (syntactic) symmetry and is excluded.

assignment_weight_inventory

The weight inventory of a formula’s variable symmetry: entry w is the number of essentially- distinct (modulo symmetry) {0,1} assignments to the variables with exactly w ones — the weighted Pólya refinement of SymmetryProfile::assignment_orbits (which is the sum). None when the group is too large to enumerate.

association_scheme_eigenmatrix

The eigenmatrix (P-matrix) of the association scheme of a formula’s variable symmetry — the scheme’s “character table”. The coherent configuration (coherent_configuration_constants) yields a commutative algebra spanned by the relation matrices A_i (A_i A_j = Σ_k a_{ijk} A_k); its intersection matrices B_i (B_i[k][j] = a_{ijk}) commute and are simultaneously diagonalizable, and P[m][i] is the eigenvalue of A_i on the m-th common eigenspace. Computed exactly over a GF(p) chosen (by search) so the algebra splits — Dixon’s method applied to the scheme. Returns (prime, P).

association_scheme_multiplicities

The multiplicities of the association scheme — the dimensions m_j of the common eigenspaces of the relation matrices in the full |X|-dimensional space; the “degrees” of the scheme, dual to the valencies. From the eigenmatrix P (#eigenmatrix) and the scheme orthogonality relation m_j = |X| / Σ_i P[j][i]·P[j][ī]/k_i (k_i = valency, ī = transpose relation). Computed exactly over a GF(p) chosen to split the algebra AND exceed |X| (so the small positive integer m_j ≤ |X| decodes uniquely). Returns the multiplicities sorted ascending.

automorphism_group_order

The order of Aut(G) for a formula’s variable-symmetry group G — the automorphism group of the symmetry itself. None when out of range.

break_all_symmetry

Iterated symmetry breaking to a fixpoint — the automated breaker. Repeatedly detect the formula’s variable symmetry and break each generator with one sound lex constraint — x_v ≤ x_{g[v]} at g’s least moved point v (v < g[v], and the lex-minimum of g’s orbit satisfies it, so it keeps ≥ 1 model per orbit, no auxiliary variables) — then re-detect on the strengthened formula, so symmetry that earlier breaks expose is broken in its turn. It runs until a round adds no new constraint: the symmetry “broken to conclusion.” Sound: every clause breaks a genuine symmetry of the current formula, so each round is equisatisfiability-preserving and the whole is equisatisfiable with the input. Returns the original clauses plus the accumulated breaks; the residual variable-symmetry group has shrunk (to trivial when single-bit breaks suffice). Solve the result with solve_comprehensive.

break_all_symmetry_complete

Complete symmetry breaking — the breaker driven all the way to a single representative per orbit. Detect the full variable-symmetry group and add the COMPLETE lex-leader (one a ≤_lex a∘g per group element, via the standard lex-chain auxiliaries), which admits exactly one model per symmetry orbit when the group is enumerable. Returns the strengthened clauses and the new variable count (originals + auxiliaries). Sound (equisatisfiable with the input); complete for groups up to the enumeration cap, and a sound partial break (generators ∪ coset representatives) for larger ones. Unlike break_all_symmetry (aux-free, complete only for fully-symmetric orbits), this leaves no residual orbit symmetry.

burnside_ring_product

The Burnside ring multiplication of a formula’s variable-symmetry group — N[a][b][l], the decomposition of the product G-set (G/H_a)×(G/H_b) into transitive G-sets (the G-set analogue of the character table’s fusion ring). None when the subgroup lattice is out of range.

canonical_form

The canonical form of a formula’s variable structure, computed by individualization–refinement (the algorithm behind nauty/saucy/bliss). It is an isomorphism invariant: two formulas equal up to a variable permutation that preserves the clause structure have the same canonical form, and — since I-R is complete — two that are not get different canonical forms (so it decides isomorphism exactly, unlike Weisfeiler–Leman). Built on color_refinement as its refinement step. None if the search exceeds its node budget (gate to moderate num_vars).

character_table

The character table of a formula’s variable-symmetry group, computed exactly over a finite field by the Burnside–Dixon algorithm (degrees + GF(p)-valued irreducible characters). The deepest structural view of the symmetry — None when the group is too large for the finite-field diagonalisation.

class_algebra_constants

The class-algebra structure constants of a formula’s variable-symmetry group — a[i][j][k], the multiplication coefficients of the conjugacy classes (Cᵢ·Cⱼ = Σₖ a[i][j][k]·Cₖ), the foundation of the character table. None when the group is too large to enumerate.

coherent_configuration_constants

The coherent configuration (association scheme) that 2-WL stabilizes into: its d basis relations (the stable pair-color classes R_0,…,R_{d-1}) and their intersection numbers p[i][j][k] = |{z : (x,z) ∈ R_i and (z,y) ∈ R_j}| for any (x,y) ∈ R_k. Returns (d, p).

coherent_rank

The rank of the coherent configuration — the number of basis relations (d), the dimension of the coherent algebra. Equal to two_wl_pair_cells; for a group’s orbital configuration it is the orbital rank. None when the configuration is out of range / not coherent.

color_refinement

Color refinement (1-dimensional Weisfeiler–Leman) of a formula’s variable–clause incidence graph — the coarsest equitable partition of the variables, computed in polynomial time. Variables and clauses are coloured (clauses initialised by width); each round recolours a clause by the sorted multiset of its incident (variable colour, sign) pairs and a variable by the sorted multiset of its incident (clause colour, sign) pairs, to a fixpoint. The result cell[v] is the variable’s colour.

color_refinement_cells

The number of cells in the color-refinement (equitable) partition — a cheap polynomial symmetry indicator. At most the number of variable orbits (cells ≤ orbits, since each cell is a union of orbits).

common_automorphism_generators

The common variable automorphisms of two formulas — phase-free permutations σ with σ(F)=F AND σ(S)=S, a generating set for a subgroup of Aut(F) ∩ Aut(S). Detected from each formula’s own automorphisms and then VERIFIED against both clause sets, so every returned generator is a genuine common automorphism (a wrong one can never slip through). This is the group under which a disagreement between F and S is symmetric: if σ fixes both, then F and S disagree at a iff they disagree at σ(a) — so equivalence checking can be reduced along its orbits.

equivalence_check_counts

(checks_with_symmetry, naive_checks) — the number of entailment checks the symmetry reduction performs (one per clause-orbit, both directions) versus the naive per-clause count. Equal when there is no usable common symmetry; strictly smaller when the shared automorphism group fuses clauses into orbits.

equivalent_modulo_symmetry

Logical equivalence F ≡ S, symmetry-reduced. F ≡ S iff F ⊨ S and S ⊨ F, and F ⊨ S iff F entails every clause of S. The key reduction: for a common automorphism σ ∈ Aut(F) ∩ Aut(S), F ⊨ C ⟺ F ⊨ σ(C) (a model of F ∧ ¬C maps under σ to a model of F ∧ ¬σ(C)), so it suffices to check one clause per orbit of S’s clauses under the common symmetry (and dually for F). The verdict is unchanged from the naive check — only the work shrinks — and a Differ witness is a concrete, re-checkable disagreement (it satisfies one formula and violates a clause of the other). This is the symmetry-aware companion to crate::sat::prove_equivalence.

formulas_isomorphic

Whether two formulas over the same variables are isomorphic — equal up to a variable permutation preserving the (signed) clause structure — by comparing their canonical forms. None if either canonical form exceeds the search budget.

fractional_automorphism

A fractional automorphism of a formula: a doubly-stochastic matrix B commuting with the variable co-occurrence matrix A (BA = AB) — the LP relaxation of an automorphism (a permutation matrix commuting with A). The canonical one is block-averaging over the coarsest equitable partition ([equitable_partition_of]): B[u][v] = 1/|cell(u)| if u,v share a cell, else 0. By Tinhofer’s theorem it commutes with A iff the partition is equitable, and it is non-trivial (not a permutation) exactly when the partition is non-discrete — i.e. exactly when the formula has non-trivial 1-WL symmetry.

frobenius_schur_indicators

The Frobenius–Schur indicators of a formula’s variable-symmetry group — +1/0/−1 per irreducible (real/complex/quaternionic), the finest representation-theoretic refinement of the symmetry (it separates groups even when the character table cannot). None when out of range.

galois_class_orbits

The Galois orbits on conjugacy classes of a formula’s variable symmetry — classes fused by the (ℤ/e)* action C ↦ C^t (algebraic conjugacy). The singletons are the rational classes. None when out of range.

generating_tuple_count

The number of ordered k-tuples of symmetries that generate the whole variable-symmetry group G (Hall’s Eulerian function e_k(G)); e_k(G)/|G|^k is the probability k random symmetries generate it. None when out of range.

is_fractional_automorphism

Verify that block-averaging over partition gives a doubly-stochastic matrix B commuting with the co-occurrence matrix A. B is doubly-stochastic by construction (each row/column sums to 1), so this checks BA = AB, which holds iff partition is equitable — the exact (integer) certificate. The identity (1/|cell(u)|)·Σ_{x∈cell(u)} A[x][w] = (1/|cell(w)|)·Σ_{x∈cell(w)} A[u][x] is verified cross-multiplied.

isotypic_multiplicities

The isotypic decomposition of a formula’s variable-permutation representation — the multiplicity of each irreducible in π = Σ_s m_s χ_s. The representation-theoretic spectrum of the symmetry, tying the character table back to the orbit/orbital structure of the action. None when out of range.

mine_clauses

The clause-bundle pass. Run every structure-mining contributor and union the implied clauses (no-goods) they discover. Each contributor’s soundness contract: every returned clause is implied by the formula, so the union preserves the solution set — a sound, never-worse enrichment that lets one method’s discovered structure accelerate the others (and CDCL). Contributors that find nothing are cheap, so this is safe to run before the fallback on any instance.

mobius_number

The Möbius number μ(1, G) of the subgroup lattice of a formula’s variable-symmetry group. None when the subgroup lattice is out of range.

models_up_to_symmetry

Enumerate the solution set up to symmetry, and count it exactly. Find a model (via the full arsenal), record it as an orbit representative, then BLOCK its entire symmetry orbit and repeat until unsatisfiable. Because every orbit is removed in one step, the representatives are the essentially- distinct solutions and the exact model count is the sum of the orbit sizes — so an instance with 2^Θ(n) models is counted by enumerating only its (far fewer) orbits. Sound: each representative is a re-checked model, each orbit a genuine set of models (the generators are automorphisms), so the orbits partition the model set. The representative count agrees with Burnside (crate::sym_break::count_models_modulo_symmetry) — two independent routes to the orbit count.

optimization_symmetry_generators

The symmetries of an optimization problem (F, weights): variable automorphisms of F that also preserve the objective (weights[g[v]] = weights[v] for all v). Under such a σ the objective is constant on orbits, so every optimal model’s whole orbit is optimal — the group along which the optimum may be symmetry-reduced. Verified against both F and the weights, so every generator is genuine.

optimize_enumeration_counts

(models_with_symmetry, models_without_symmetry) — how many candidate models the optimizer enumerates with the symmetry break versus the naive enumeration. Equal with no usable symmetry, smaller when the objective-preserving group fuses optimal (and non-optimal) models into orbits.

optimize_modulo_symmetry

Weighted minimization, symmetry-reduced. Minimise Σ weights[i]·x_i over the models of clauses, exploiting optimization_symmetry_generators: break the objective-preserving symmetry, then search the reduced model space. SOUND — the optimum is identical to the unbroken problem (an optimal orbit’s lex-leader survives the break and has the same objective) and the witness is a genuine model of the original F. None iff F is unsatisfiable. The symmetry-aware optimizer (a new problem class beyond the decision/counting/equivalence faces).

pb_symmetry_profile

The SymmetryProfile of a pseudo-Boolean system’s coefficient-symmetry group — variables that share a coefficient profile across all constraints (crate::pseudo_boolean::coeff_symmetry_generators) — read through the same structural ladder as symmetry_structure. The symmetry of weighted constraints, surfaced exactly like the clause-structure symmetry.

permutation_character

The permutation character π(g) = #fixed variables of g of a formula’s variable-symmetry action, valued per conjugacy class. The character of the representation the symmetry group carries on the variables themselves. None when the group is too large to enumerate.

permutation_character_decomposition

The permutation-character decomposition of a formula’s variable-symmetry group — the bridge between its table of marks and its character table. M[i][s] is the multiplicity of irreducible χ_s in the permutation representation on the cosets G/H_i (Frobenius reciprocity). Returns (subgroup_orders, irreducible_degrees, M). None when out of range.

provably_asymmetric_variables

The variables that color refinement places in a singleton cell — provably fixed by every (phase-free) automorphism, since orbit(v) ⊆ cell(v) and |cell(v)| = 1 forces |orbit(v)| = 1. A polynomial certificate of asymmetry: these variables can be skipped entirely when detecting or breaking symmetry.

semantic_symmetry_pairs

The semantic symmetries (variable transpositions) of a CNF: pairs (a,b) whose swap preserves the MODEL SET, F ≡ swap(F), even when it does NOT preserve the clause set. Checked by implication: F ⊨ swap(F) (and, by the involution swap² = id, that is full equivalence). Returns the semantic pairs and whether any is non-syntactic (clause set changed) — i.e. genuinely beyond what the syntactic detector (crate::sym_break::variable_automorphism_generators) can see.

solve_by_components

Decide via plain component decomposition as a public dispatcher route: split into independent components and solve each apart through the full arsenal, combining the verdicts. A single component (or a model that fails the fail-closed recheck) defers to the plain CDCL fallback.

solve_by_symmetry_breaking

Solve by breaking all symmetry first — the breaker as a front-end. Run the aux-free recursive breaker (break_all_symmetry) to collapse the symmetry to its fixpoint, then decide the reduced formula with the full arsenal (solve_comprehensive). Equisatisfiable, so the verdict is the original’s, and any returned model satisfies the original clauses (a subset of the broken set) — re-checked fail-closed. (Uses the aux-free reducer, not break_all_symmetry_complete: CDCL handles the residual cheaply, and the complete lex-leader of a large group would be far more expensive than the search it saves.)

solve_comprehensive

The full arsenal in one call — the opt-in power-mode solver. Runs the cheap specialists (structured_prefix); then, before the exponential CDCL fallback, the heavier engines the fast path skips: bounded-degree Nullstellensatz / Polynomial Calculus (the nonlinear algebraic refutation, crate::polycalc) and complete lex-leader symmetry breaking (crate::sym_break: the whole automorphism group from the Schreier–Sims backend, feeding CDCL a one-model-per-orbit formula). Slower than solve_structured (it may run Nullstellensatz and automorphism detection), so it is the maximum-power entry, not the default. Always correct — the CDCL fallback is complete.

solve_structured

Decide clauses over num_vars variables, routing through every cheap specialist before CDCL — the fast default front-end. For the full arsenal (heavy algebraic + complete symmetry breaking before the fallback) use solve_comprehensive.

solve_with_declared_symmetry

The full arsenal with caller-DECLARED symmetry. The modeler often knows symmetries the automatic detector cannot afford to find (geometric, semantic, or simply large). This entry point accepts declared variable-permutation generators, verifies each is a genuine symmetry ([is_declared_symmetry] — never trusting a declaration blindly, so an incorrect one is silently dropped), unions the survivors with the auto-detected symmetry, and breaks the combined group with the lex-leader (complete by enumeration when the group is small, partial over the generators otherwise). Sound: only verified, model-set- preserving permutations enter the break; a SAT model is re-checked, and on any anomaly it falls back to the authoritative solve_comprehensive. With no declared and no detected symmetry it simply is solve_comprehensive.

structured_prefix

The cheap-specialist chain — every route O(clauses) to apply and reject, so the front-end is never slower than plain CDCL. Returns the decision if a specialist fires, or None (the CDCL fallback is needed). Public so callers that only want the O(clauses) specialist verdict — e.g. a per-node cofactor-DAG leaf check — can skip the expensive CDCL search entirely.

symmetry_structure

Compute the SymmetryProfile of clauses — detect the variable-symmetry generators and read off the whole structural ladder (order via Schreier–Sims, orbits, orbitals/rank, transitivity, primitivity, blocks). The rank and transitivity rungs are gated to moderate sizes (their tuple spaces grow with the degree); 0 signals “not computed” there.

table_of_marks

The table of marks of a formula’s variable-symmetry group — the Burnside-ring classification of its G-sets (the permutation-representation analogue of character_table). Returns (subgroup_class_orders, marks). None when the subgroup lattice is out of range.

tensor_decomposition

The tensor (fusion) decomposition of a formula’s variable-symmetry irreducibles — N[i][j][k], the multiplicity of χ_k in χ_i ⊗ χ_j, the multiplication table of the representation ring R(G). None when the character table is out of range.

three_wl_colors

3-dimensional Weisfeiler–Leman (3-WL) of a formula’s variables — color refinement on ordered triples. A triple (i,j,k) is initialized by the 2-WL colors of its three pairs (pc[i][j], pc[i][k], pc[j][k]), then each round recolored by (old color, sorted multiset over all w of (color(w,j,k), color(i,w,k), color(i,j,w))) to a fixpoint. Returns the n×n×n color tensor.

three_wl_fingerprint

The label-independent 3-WL fingerprint: the sorted multiset of triple-color class sizes. Separates strongly-regular graphs that share every 2-WL invariant (the rook’s vs Shrikhande graph).

two_wl_fingerprint

The label-independent 2-WL fingerprint: the sorted multiset of pair-color class sizes. Two formulas with different fingerprints are provably non-isomorphic (as colored variable structures) — the distinguishing power that separates, e.g., a 6-cycle from two triangles where 1-WL cannot.

two_wl_pair_cells

The number of distinct 2-WL pair colors — at most the number of orbitals (pair-cells ≤ orbitals).

two_wl_pair_colors

2-dimensional Weisfeiler–Leman (2-WL) of a formula’s variables — color refinement lifted from vertices to ordered pairs. Each pair (i,j) is colored: the diagonal by its 1-WL vertex color, an off-diagonal pair by (1-WL(i), 1-WL(j), co-occurrence signature) where the signature is the sorted multiset over clauses containing both of (clause width, sign of i, sign of j). Each round recolors (i,j) by (old color, sorted multiset over all k of (color(i,k), color(k,j))), to a fixpoint.

weighted_model_count

Symmetry-accelerated weighted model counting — the partition function Z = Σ_{m ⊨ F} W(m) with literal weights W(m) = Π_v weight[v].{1 if m[v] else 0}. The formula’s variable symmetry partitions the models into orbits, so each solve() recovers one model, its whole orbit is enumerated and its members’ weights summed, then the entire orbit is blocked — one solve per orbit instead of per model. Exact for ARBITRARY weights (every model’s true weight is summed; the symmetry only groups the search), the symmetry-aware analogue of weighted #SAT / lifted inference. Returns Z.

weighted_model_count_solve_counts

(orbit_solves, total_models) — how many solve() calls the symmetry-accelerated weighted count makes (one per model-orbit) versus the number of models. Equal with no usable symmetry, smaller when symmetry fuses models into orbits.