Research map / Learning theory and algorithms / Combinatorial and search optimization
SAT-Based Techniques for Lexicographically Smallest 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.
Proposes SAT-based gradual-construction algorithm (mlex) with propagation techniques (budgeting, invariants, idempotent apex, binary search) to compute the lexicographically smallest representative of finite magmas and algebraic structures.
Problem
Computing the lexicographically smallest isomorphic representative (normal form) of finite algebraic structures such as groups, loops, quasigroups, semigroups and magmas, which an explicit SAT encoding handles poorly due to its size and hard counting-based SAT calls.
Approach
Instead of encoding the unknown target table explicitly, construct the lexmin table cell by cell via SAT queries over an unknown permutation, and prune SAT calls with counting-based budgets, isomorphism-invariant row matching, idempotent-apex first-row identification, upper bounds from models, and a modified binary search over disjunctions of values.
Key results
- Budgeting is the most significant technique in the ablation; the all-enhancements version is the fastest and most robust.
- Explicit encoding was excluded because it used dozens of gigabytes of memory even for small problems.
- Smallsemi's lexmin function suffered timeouts and high memory even at order 20.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add budgeting propagation (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | Helped |
| Use modified binary search instead of linear UNSAT-SAT search (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | Helped |
| Add first-row identification (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | No clear effect |
| Add row invariants (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | No clear effect |
| Add mid-row budgeting refinement (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | No clear effect |
| Add the upper bound by last value (ablation) | mlex · Random algebra samples, orders 16–256 | instances solved within 30 minutes | No clear effect |
| Enable all propagation and search enhancements | mlex · Random algebra samples, orders 16–256 | runtime | Helped |
| Use cadical instead of minisat | mlex with enhancements turned on · Random algebra samples, orders 16–256 | runtime | Mixed |
Surprising findings
- Cadical performs poorly compared to minisat when all improvements are turned off.
- Standard binary search did not perform well in experiments, motivating a modified binary search.
Limitations
- Currently supports only a single binary operation; multi-table structures are future work.
- Worst-case O(|D|^3) SAT calls and hard pigeonhole-style SAT calls can stall individual cells.
- Evaluated on random samples only, up to order 256.
Experimental setup
Datasets: randomly generated groups (GAP AllSmallGroups) random magmas, semigroups, quasigroups, loops (GAP Random, RandomQuasigroup, RandomLoop)
Benchmarks: 210 random algebras of orders 16-128 across five structures, plus 5 magmas each of orders 192 and 256
Metrics: number solved within 30-minute timeout runtime (cactus plots)
Baselines: Explicit Encoding Smallsemi GAP lexmin basic gradual construction (Algorithm 1) linear UNSAT-SAT search
Builds on: Explicit SAT encoding of isomorphism nauty canonical labeling MaxSAT iterative techniques
Closest papers by meaning
- Complete Symmetry Breaking for Finite Models (AAAI 2025 · similarity 0.90)
- An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes (AAAI 2024 · similarity 0.85)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.84)
- Using Symmetries to Lift Satisfiability Checking (AAAI 2024 · similarity 0.84)
- Machine Learning meets Algebraic Combinatorics: A Suite of Datasets Capturing Research-level Conjecturing Ability in Pure Mathematics (ICML 2025 · similarity 0.83)
- A SAT + Computer Algebra System Verification of the Ramsey Problem R(3, 8) (Student Abstract) (AAAI 2024 · similarity 0.83)
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.