# AI for Science: SAT Modulo Symmetries

**Last updated**: 2025-10-31

Stefan Szeider's research applies AI techniques, particularly SAT solving, to long-standing problems in mathematics and theoretical computer science. The SAT Modulo Symmetries (SMS) framework has been used to discover new mathematical results in extremal graph theory, Ramsey theory, matroid theory, and quantum foundations.

## The SAT Modulo Symmetries Framework

SAT Modulo Symmetries (SMS) combines SAT solving with dynamic symmetry breaking for isomorph-free generation of combinatorial objects.

### The Challenge

Many problems in discrete mathematics involve searching for combinatorial objects with specific properties. The number of objects grows exponentially—for graphs with 11 vertices, there are approximately 3.6 × 10^16 labeled graphs but only 1.02 × 10^9 non-isomorphic graphs. Without handling symmetries, SAT solvers redundantly explore different labelings of the same structure.

### How SMS Works

SMS augments a CDCL SAT solver with a custom propagator (MinCheck) that checks canonicity of partially constructed objects during search:

1. The SAT solver encodes the desired property as a propositional formula
2. During search, the solver assigns variables (representing components of the object)
3. The canonicity tester checks if the partial assignment can extend to a canonical object
4. If not, it provides a learned clause that prunes that region of the search space

This dynamic symmetry breaking avoids limitations of static methods, which must rely on incomplete symmetry breaking.

### Key Innovation

Rather than adding all canonicity constraints to the initial formula (which would be exponentially large), SMS checks canonicity on-the-fly during solver execution using a tractable relaxation: finding a single permutation that certifies non-canonicity for all possible extensions of the partial object. This provides complete symmetry breaking without the overhead of encoding all constraints upfront.

## Applications and Results

### Extremal Graph Theory

**Triangle-free graphs**: SMS found the smallest triangle-free graphs with high chromatic number. The smallest triangle-free graph that is non-3-colorable is the Grötzsch graph (11 vertices).

**Graph coloring**: Discovery of new extremal examples for various graph coloring problems.

**Diameter-2-critical graphs**: Verified the Simon-Murty Conjecture for graphs up to 19 vertices.

**Cubic graphs**: Verified the 3-Decomposition Conjecture for cubic graphs up to 28 vertices.

### Ramsey Theory

**Ramsey numbers**: Computational search for Ramsey number bounds using SMS to avoid isomorphic configurations.

**Graph Ramsey problems**: Finding witness graphs for Ramsey-theoretic questions.

### Matroid Theory

**Matroid generation**: Isomorph-free generation of matroids with specific properties.

**Rota's Basis Conjecture**: Proved the conjecture for rank 4 matroids using SMS.

### Quantum Foundations

**Kochen-Specker systems**: SMS improved the lower bound for the minimum number of vectors in a Kochen-Specker system from 23 to 24 vectors. These systems demonstrate quantum contextuality in measurement.

### Planar Graph Problems

**Diameter-2-critical graphs**: Verification of the Simon-Murty Conjecture for graphs up to 19 vertices.

### Computational Social Choice

**EFX allocations**: Envy-free up to any item allocations in fair division problems.

### Minimal Unsatisfiable CNFs

Finding minimal unsatisfiable CNF formulas with specific properties.

## Survey Paper

**SAT Modulo Symmetries: A Survey** (Invited Talk)
Stefan Szeider
*SC² 2025: 10th International Workshop on Satisfiability Checking and Symbolic Computation* (affiliated with CADE 2025), August 2, 2025, Stuttgart, Germany
Survey of the SMS framework and its applications to problems in discrete mathematics, including extremal graph theory, Ramsey theory, matroid theory, and quantum foundations.

## Related Work

The SMS approach builds on:
- **Conflict-Driven Clause Learning (CDCL)**: Modern SAT solving technique
- **Isomorph-free generation**: Classical techniques from computational group theory
- **Symmetry breaking**: Static and dynamic methods for handling symmetries in SAT

## Implementation

SMS is implemented as an extension to standard CDCL SAT solvers using the IPASIR-UP interface, which allows external propagators to communicate with the solver through callbacks.

The system consists of:
- **Standard CDCL SAT solver**: Operates on CNF encoding of the property
- **MinCheck canonicity tester**: Analyzes partial assignments for canonicity
- **IPASIR-UP interface**: Callback-based communication between solver and propagator
- **Specialized propagators**: Domain-specific propagators (e.g., lazy Kuratowski-based propagator for planar graphs)
- **PySMS Python wrapper**: User-facing interface (`pysms.graph_builder`) for building problem instances

### Advanced Features

**Co-Certificate Learning (CCL)**: A dual-solver architecture that extends SMS to handle coNP properties (like non-3-colorability). CCL allows SMS to address problems defined by the absence of certain structures, as well as their presence.

**Proof Generation**: SMS produces verifiable DRAT proofs and nc-certificates that certify both correctness (found objects satisfy the property) and completeness (all canonical objects were explored). This enables independent verification of results.

## Impact on Mathematics

SMS has enabled computational exploration of mathematical questions that were computationally infeasible with prior approaches:

**Automation**: Transforming mathematical conjectures into SAT instances that can be automatically solved

**Discovery**: Finding new mathematical objects and counterexamples

**Verification**: Proving non-existence results by exhaustive isomorph-free search

**Scaling**: Handling problem sizes beyond what enumeration-based methods can reach

## Theoretical Foundations

**Canonicity**: An object is canonical if it is the lexicographically minimal representative of its isomorphism class.

**Tractable relaxation**: Rather than directly testing whether a partially defined object can be extended to canonical (which is computationally difficult), SMS finds a single permutation that certifies non-canonicity for all possible extensions of the partial object. This tractable test is central to the method's efficiency.

**Learned clauses**: When a partial assignment cannot extend to canonical, SMS generates a clause that prevents the solver from exploring that subspace.

**Certified canonical property**: A partially defined object is certified canonical if no permutation can map it to a lexicographically smaller partial object that agrees on defined positions.

## Comparison with Other Approaches

**Static symmetry breaking**: Adds constraints to initial formula but must use incomplete breaking
- SMS advantage: Complete symmetry breaking without exponential blowup

**Enumeration**: Generate all canonical objects explicitly
- SMS advantage: Avoids enumeration, directly searches for objects with desired properties

**Symmetry breaking during search (BreakID, etc.)**: Dynamic methods using orbital reasoning
- SMS distinction: Uses canonicity testing rather than orbital computation

## Future Directions

- Extending to other combinatorial structures (permutations, partitions, designs)
- Integration with SMT solvers for richer theories
- Parallel and distributed versions for larger problem instances
- Application to optimization problems (finding extremal objects)

## Collaborators

This research is joint work with:
- Markus Kirchweger (TU Wien)
- And collaborators in mathematics and quantum foundations

## Publications

SMS framework introduced in:
- Kirchweger, Szeider (2021): Initial SMS framework
- Kirchweger, Szeider (2024): Extended framework and applications

**Contact**: sz@ac.tuwien.ac.at | [DBLP](https://dblp.org/pid/s/StefanSzeider.html)