Research map / Learning theory and algorithms / Combinatorial and search optimization
Complete Symmetry Breaking for Finite Models
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces a SAT-based method that computes compact complete lex-leader symmetry breaks for finite magmas defined by first-order axioms, enabling model counting of non-isomorphic algebras without enumeration.
Problem
Counting or enumerating non-isomorphic finite algebraic structures (magmas and subclasses) suffers from huge numbers of isomorphic copies; existing symmetry breaks are partial or class-specific.
Approach
Generalizes the graph canonizing-set algorithm to arbitrary FOL-defined magma classes: iteratively adds counterexample permutations via SAT until a canonizing set is obtained, then reduces it, so that model counting of the resulting SAT formula yields isomorphism-class counts.
Key results
- Obtained new counts of non-isomorphic AG-groupoids for n=7 (about 6.4e11 models for AG-groupoids at n=7 by the table) where pure enumeration only reached n=6.
- Implication zroupoids counted for n=7 and rectangular groupoids for n=6, both not in the literature; the AG-groupoid canonizing set for n=7 has 240 permutations versus 7! = 5040.
- Diagonal vectorization yields smaller canonizing sets than row-by-row in most cases, and the canonizing set for groups of order 10 needs only 18 permutations.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use diagonal ordering instead of row-by-row ordering | Complete symmetry breaking for finite algebra classes · Algebra classes in the experiments | canonizing-set size | Helped |
| Use diagonal ordering instead of row-by-row ordering | Complete symmetry breaking + d4 · Algebra classes in the experiments | model-counting runtime | Mixed |
| Use diagonal ordering instead of row-by-row ordering | Complete symmetry breaking + d4 · Implication zroupoid, size 7; rectangular groupoid, size 6 | model-counting feasibility | Helped |
Surprising findings
- Diagonal-first vectorization gives smaller canonizing sets than row-by-row, though the authors leave the reason for future work.
- Breaking by transpositions only is strictly stronger than the least number heuristic, which the paper proves.
Limitations
- Canonizing set computation often hits time or memory limits, so results stop at n=6 to 8 for most classes.
- Only single-binary-operation structures (magmas) are supported; multiple function symbols are future work.
- Lower bounds and NP-hardness of deciding lex-leaders for magmas are not proven.
Experimental setup
Datasets: FOL axiomatizations of algebra classes (AG-groupoids, commutative quasigroups, groups, semigroups, inverse semigroups, e
Benchmarks: counts of non-isomorphic algebras for domain sizes 2-10 across 14 algebra classes OEIS sequences
Metrics: canonizing set size computation time model count model counter time
Baselines: least number heuristic transposition-based symmetry breaking pure enumeration
Builds on: canonizing sets for graphs least number heuristic d4 model counter PySAT
Closest papers by meaning
- SAT-Based Techniques for Lexicographically Smallest Finite Models (AAAI 2024 · similarity 0.90)
- Breaking Symmetries in Quantified Graph Search: A Comparative Study (AAAI 2025 · similarity 0.84)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.83)
- Using Symmetries to Lift Satisfiability Checking (AAAI 2024 · similarity 0.83)
- Exploiting Symmetries in MUS Computation (AAAI 2025 · similarity 0.83)
- Engineering an Exact Pseudo-Boolean Model Counter (AAAI 2024 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.