The generation of combinatorial objects with a given property is a fundamental task in discrete mathematics and computer science. The combinatorial explosion of candidate objects renders simple generate-and-test approaches infeasible. SAT-based synthesis methods ofer an alternative, but they require efective symmetry breaking to prevent the solver from exploring isomorphic parts of the search space. This paper surveys SAT Modulo Symmetries (SMS), a framework that integrates dynamic symmetry breaking directly into a Conflict-Driven Clause Learning (CDCL) SAT solver. The approach relies on a propagator that checks for the canonicity of partially defined objects during the search. If a partial assignment cannot be extended to a canonical object, the propagator provides a learned clause to the solver, pruning the corresponding part of the search tree. We outline the core components of the SMS framework and review its application to several open problems in areas such as extremal graph theory, Ramsey theory, matroid theory, and quantum foundations, where it has been used to obtain new mathematical results.
same structure, difering only in how vertices are labeled. A graph is considered canonical if it is selected as the unique representative of its isomorphism class; for instance, if its adjacency matrix is lexicographically minimal among all labelings. For = 11 the number of non-isomorphic graphs is approximately 1.02 × 10 9,2 compared to 3.6 × 10 16 labeled graphs—a reduction by seven orders of magnitude. However, this is still a very large number. The standard way to answer the above question about the smallest triangle-free graph that is non-3-colorable would be to enumerate all canonical graphs with ≤ 11 vertices and check for each whether it is triangle-free and non-3-colorable. This approach is limited to where it is still feasible to enumerate.
An alternative that avoids enumeration is to formulate the problem as a synthesis task using
propositional satisfiability (SAT) solvers. Here, one defines propositional variables to represent the components
of the object (e.g., , stating whether the edge between vertices and exists) and encodes the
desired property as a propositional formula. A satisfying assignment to the formula corresponds to an
object with the property. Modern SAT solvers based on Conflict-Driven Clause Learning (CDCL) can
explore vast search spaces [
Static symmetry breaking, where canonicity constraints are added to the initial propositional formula,
provides a partial solution. However, a polynomial-size encoding for full canonicity is not known,
so these approaches must rely on incomplete symmetry breaking, which may still generate multiple
isomorphic copies [
This paper surveys SAT Modulo Symmetries (SMS), a framework for isomorph-free generation that
implements dynamic and complete symmetry breaking within a CDCL SAT solver. It avoids the
limitations of static methods by interacting with the solver during its search, pruning branches that are
guaranteed not to lead to canonical solutions. SMS was originally introduced at CP 2021 [
We describe the SMS framework and review its application to a range of problems in combinatorics and related fields.
The central idea of SMS is to augment a CDCL SAT solver with a custom propagator that performs canonicity tests on-the-fly.
The SMS architecture consists of two main components: (1) a standard CDCL SAT solver that operates on a formula encoding the desired property of the combinatorial object, and (2) symmetry-breaking propagator MinCheck, or canonicity tester, that communicates with the solver through a callback-based interface.
During its search, the SAT solver makes decisions, assigning truth values to variables. These assignments correspond to a partially constructed object. At certain points, the solver queries the propagator. The propagator analyzes the current partially defined object for canonicity. If it determines that the partially defined object cannot be extended to any canonical solution, it learns a blocking clause. This clause is passed back to the SAT solver, which uses it to backtrack and prune that entire region of the search space.
A key concept in SMS is the partially defined graph. At any point during the solver’s execution, the set of edge variables is partitioned into those assigned true, those assigned false, and those that are unassigned. This corresponds to a graph where the edge set is partitioned into a set () of defined CDCL SAT
solver partially defined learns a clause if is not
graph IPASIR-UP certified canonical graph property in CNF result edges, a set () of undefined edges, and the remaining defined non-edges. Such a graph represents the set () of all fully defined graphs that can be obtained by assigning the variables corresponding to edges in (). In the adjacency matrix representation shown in Figure 3, entries are 1 for edges, 0 for non-edges, and ⋆ for undefined edges.
1 5
2 4 3
A partially defined graph 1 is a refinement of 2 (written 1 ⊒ 2) if more edges are defined in 1, meaning (1) ⊆ ( 2).
The goal is to prune the search as soon as the current partially defined graph is provably noncanonical. Ideally, one would terminate a search branch if for every possible extension ∈ (), there exists a permutation such that () is lexicographically smaller than . (Here, lexicographic order compares adjacency matrices row-major, reading the full symmetric matrix including the diagonal.) However, checking this property is computationally dificult, as it involves quantifiers over exponentially large sets of graphs and permutations.
SMS employs a more tractable relaxation of this condition. It searches for a single permutation that acts as a certificate of non-canonicity (or nc-certificate) for the entire set (). That is, it checks if: There exists a permutation such that for all extensions ∈ (), the adjacency matrix of () is lexicographically smaller than the adjacency matrix of .
This condition, with its swapped quantifiers, is suficient to prove that no extension of can be canonical. While this check is a relaxation, it becomes equivalent to the full canonicity test when the graph is fully defined (i.e., () = ∅). Thus, the method is sound (it never prunes canonical solutions) and complete (it finds all canonical solutions).
We now describe how SMS searches for an nc-certificate by exploring a refined space of permutations using ordered partitions. The heart of SMS is the canonicity tester MinCheck , which searches for an nc-certificate . This search is structured using ordered partitions of the vertex set = {1, . . . , }. An ordered partition = [1, . . . , ] is a sequence of disjoint vertex sets whose union is . It represents the set of all permutations where for any ∈ and ∈ with < , it holds that () < ().
The algorithm proceeds recursively: 1. It starts with the trivial partition [{1, . . . , }], which represents all ! permutations. 2. It refines the partition by making decisions. For instance, if the current partition is [{1, 2, 3}, {4, 5}] and we decide to map vertex 2 to position 1, we obtain the refined partition [{2}, {1, 3}, {4, 5}]. 3. After each decision, it propagates constraints derived from the structure of the partially defined graph to further refine the other sets in the partition, reducing the set of candidate permutations. This structured search continues until an nc-certificate is found or the search space of permutations is exhausted for the current branch. In the worst case, the search is exponential, but due to the propagation, it often runs quickly.
If an nc-certificate is found for a partially defined graph , the algorithm identifies a minimal non-canonical subgraph ′ with ⊒ ′, called an obstruction. From this obstruction, a blocking clause is generated. For instance, the clause
⋁︁ ∈(′) ¬, ∨
⋁︁ ∈/(′)∪(′) , is added to the solver. This clause blocks ′ and all its extensions, efectively pruning the search.
The core SMS framework described in the previous section has been extended in several directions to enhance its capabilities and broaden its applicability.
The SMS framework can be extended with domain-specific propagators that encode graph-theoretic lemmas directly into the search process, building on the core MinCheck propagator (Section 2). These specialized propagators augment the canonicity tester with additional constraints derived from structural properties of the target objects. By pruning branches based on domain knowledge, they can reduce the search space beyond what pure symmetry breaking achieves.
This approach was used to partially verify the 3-Decomposition Conjecture—that every connected
cubic graph can be decomposed into a spanning tree, a collection of cycles, and a matching. Using
SMS with a specialized propagator encoding structural properties of cubic graphs, all graphs up to 28
vertices were verified, extending the previously verified bound from 20 vertices [
Many mathematical properties, such as non-3-colorability, are coNP-complete and dificult to encode
directly with SAT clauses. To address this class of problems, SMS was extended with Co-Certificate
Learning (CCL) [
The CCL framework uses a dual-solver architecture (Figure 4), complementing SMS’s symmetry pruning. SAT solver 1 generates a candidate graph satisfying a property (e.g., triangle-free). This candidate is passed to SAT solver 2, which tests whether the graph satisfies a property (e.g., 3colorability). If SAT solver 2 reports unsatisfiability (the graph does not satisfy ), then the candidate satisfies both and ¬, and a solution is found. If SAT solver 2 reports satisfiability (the graph satisfies ), it returns a co-certificate—a satisfying assignment that witnesses property . For 3colorability, a co-certificate is a valid 3-coloring.
MinCheck CDCL SAT solver 1 blocking clause candidate graph graph property in CNF graph property in CNF CDCL SAT solver 2 result
From this co-certificate, a blocking clause is constructed and learned by SAT solver 1. For a 3coloring , the clause requires that any graph considered in subsequent search must contain at least one edge between vertices that were assigned the same color by :
⋁︁ <, ()=() , This clause eliminates all graphs that satisfy the property via the same coloring , and SAT solver 1 resumes its search for a graph satisfying but not .
A key observation is that a single co-certificate can significantly reduce the search space. For
trianglefree graphs on 14 vertices, while tools like Nauty must check over 467 million canonical graphs, SMS
with CCL visits only 85,668 candidates by learning just 9,407 3-colorings from SAT solver 2. On average,
each 3-coloring eliminates approximately 50,000 canonical graphs [
A further refinement, Q-SMS, unifies this dual-solver architecture by formulating the entire problem
as a Quantified Boolean Formula (QBF) and using a circuit-based QBF solver [
The SMS framework can produce independently verifiable proofs that certify both the correctness and
completeness of its results [
For the symmetry-breaking component, SMS outputs an nc-certificate (a permutation ) for each learned symmetry-breaking clause. An independent checker can verify in polynomial time that this permutation indeed witnesses the non-canonicity of the pruned partial graph. This ensures that no canonical solution was incorrectly discarded.
For the SAT reasoning component, the framework can generate standard DRAT (Deletion Resolution
Asymmetric Tautology) proofs [
To certify the completeness of an enumeration, the framework adds blocking clauses to exclude all found solutions and verifies the unsatisfiability of the resulting formula. The DRAT proof for this extended formula certifies that no additional non-isomorphic solutions exist. Individual solutions can be certified as canonical by encoding the canonicity test as a CNF formula; a DRAT proof of unsatisfiability for this formula confirms that the solution is lexicographically minimal among all isomorphic copies.
The SMS framework has been applied to computational problems across several areas of discrete mathematics, yielding new results and confirming existing conjectures for problem sizes previously beyond the reach of prior methods.
Extremal graph theory seeks graphs that maximize or minimize a parameter subject to given constraints. One such problem concerns diameter-2-critical graphs. A graph has diameter if the longest shortest paths between any two vertices have length . A graph is diameter--critical if its diameter is , but deleting any edge increases the diameter. The Simon-Murty Conjecture (1979) states that a diameter-2critical graph on vertices has at most ⌊2/4⌋ edges.
Prior computational searches were limited to graphs with at most 11 vertices. Using a direct SAT
encoding of the diameter-2-critical property, SMS enumerated all such graphs for larger sizes. For
= 12, it found all 40,866 graphs in under a minute, and for = 13, it enumerated all 688,120 graphs
in approximately 20 minutes. Static symmetry breaking methods did not terminate for ≥ 12 . By
incorporating known degree constraints from the literature to partition the search space, the conjecture
was further verified for all ≤ 19 [
Beyond diameter-2-critical graphs, we studied extremal problems in planar graphs via planarity
encodings. The planar Turán number ex (, ) is the maximum number of edges in an -vertex
planar graph containing no subgraph isomorphic to . Computing these numbers requires generating
planar graphs with specified properties. We compared three planarity encodings: a lazy
Kuratowskibased propagator that detects forbidden Kuratowski subdivisions (topological 5 or 3,3) using the
lazy propagator approach introduced in Section 3.1, an eager encoding using Schnyder’s planarity
criterion [
This area concerns partitioning graph edges or coloring vertices under complex structural constraints.
The 3-Decomposition Conjecture, as mentioned in Section 3.1, states that every connected cubic graph
can be partitioned into a spanning tree, a collection of cycles, and a matching. Using specialized
propagators, SMS exploits theoretical properties of minimal counterexamples. A forbidden subgraph
checker, integrating the Glasgow Subgraph Solver [
A related coloring problem concerns biplanar graphs—graphs whose edges can be partitioned into
two planar graphs. The Earth-Moon problem [
These problems concern the unavoidable appearance of substructures in large combinatorial objects.
The Ramsey number (, ) is the smallest integer such that any graph on vertices contains either
a clique of size or an independent set of size . The set ℛ(, , ) consists of all non-isomorphic
graphs on vertices with no -clique and no -independent set. Using a direct encoding of these
properties, SMS enumerated the complete sets for ℛ(3, 5, ) and ℛ(4, 4, ). The framework’s ability
to produce verifiable proofs of completeness is particularly valuable in this context. The DRAT proof
from the SAT solver certifies the search, while nc-certificates for each learned symmetry clause can be
independently verified [
A related universality problem asks for the smallest graph containing all graphs of a given size. A
graph is -universal if it contains all graphs on vertices as induced subgraphs. The problem is to
ifnd the smallest such graph, denoted (). A similar problem exists for tournaments, (). SMS was
applied using both a direct SAT encoding and a lazy approach with the Glasgow Subgraph Solver as an
external propagator. A templates method, where pre-computed interactions of small pattern graphs
partition the search space for parallel execution, further improved performance. This work improved
the lower bound for 7-universal graphs, proving (7) > 16, and determined exact values () for ≤ 6
and bounded the 7-universal tournament size to 13 ≤ (7) ≤ 15 [
The SMS framework extends beyond simple graphs to more abstract combinatorial objects. For
hypergraphs, the Erdős-Faber-Lovász Conjecture (1972) concerns the edge-colorability of linear hypergraphs
(hypergraphs where each pair of edges shares at most one vertex). To apply SMS, hypergraphs are
modeled via their bipartite incidence graphs. The coNP property of non-colorability is handled using
Co-Certificate Learning. This approach verified the conjecture for all linear hypergraphs with up
to 12 vertices, extending previous computational results and providing the first such verification with
proof-generation capabilities [
For matroids, Rota’s Basis Conjecture (1989) concerns decompositions into disjoint rainbow bases. We developed a specialized MinCheck propagator, tailored to the basis exchange axioms of matroids of bounded rank. This led to a proof of the conjecture for all matroids of rank 4. The work also provided the first framework for producing DRAT proofs for matroid problems [16].
We also extended the framework to CNF formulas by encoding them as graphs. Our goal was to ifnd smallest unsatisfiable (, )-CNF formulas, where each clause has exactly literals and each variable occurs at most times. The size of these formulas relates to inapproximability results for MaxSAT. We encoded CNF formulas as 2-colored graphs (clause-literal graphs) to apply SMS. The search combined SMS with theoretical techniques like disjunctive splitting. This determined exact minimum sizes of unsatisfiable formulas for all 3-CNF subclasses and improved the upper bound for the smallest unsatisfiable (4,5)-CNF formula from Knuth’s 257 to 235 clauses [17, 18].
We also applied SMS to problems from fields outside pure combinatorics. In quantum foundations,
Kochen-Specker systems are sets of vectors that demonstrate quantum contextuality, a key distinction
between quantum and classical physics. Finding the smallest such system is a long-standing problem.
We formulated the search for a Kochen-Specker system as finding a graph with a coNP property
(non-010-colorability), which was handled via CCL (Section 3.2). A 010-coloring assigns colors 0, 1
to vectors respecting orthogonality [
In computational social choice, the rainbow cycle number () provides bounds on the feasibility of achieving envy-free-up-to-any-good (EFX) allocations in the fair division of indivisible goods. Variants () and () use edge labelings restricted to functions ↦→ + mod and permutations, respectively, with () ≤ () ≤ (). We introduced the new technique of invariant pruning: to branch on the value of a graph invariant not known a priori, such as maximum degree, reducing symmetry [20].. Using SMS with invariant pruning, we determined the exact values (4) = 4 and (5) = 5, improving guarantees for EFX allocations. Invariant pruning provided a speedup of almost two orders of magnitude in some cases.
To facilitate adoption and enable further research, the SMS framework is implemented as open source software. This section outlines its architecture and practical usage, connecting the theoretical concepts from Section 2 to their implementation. The SMS framework is available at with documentation at
The software consists of a C++ core implementation and a Python wrapper that provides a high-level interface for encoding graph properties.
The core implementation consists of the solver smsg, which is built on CaDiCaL, an award-winning CDCL SAT solver, extended with the MinCheck propagator for symmetry breaking. The integration utilizes the IPASIR-UP interface [21], which provides callback functions for communication between the solver and the propagator. When the propagator detects that a partially defined graph cannot be extended to a canonical solution, it constructs a conflict clause and passes it to the solver via cb_add_external_clause_lit.
The software also provides C++ libraries (libsms_static.a and libsms.so) for integration into other applications.
The Python module PySMS (pysms) provides a declarative interface for specifying graph properties without directly manipulating propositional variables. The module pysms.graph_builder can be invoked from the command line or imported into custom scripts. It generates CNF encodings in DIMACS format [22] , and, by default, automatically invokes smsg to solve them.
For command-line use, the basic syntax is: python -m pysms.graph_builder --vertices n [options] Common options include –all-graphs to enumerate all solutions, –delta-low d for minimum degree, –num-edges-upp e for maximum edges, and –directed for directed graphs. To output CNF without solving, add –no-solve. For better performance, it is recommended to use –cutoff 20000 to limit the minimality check due to the exponential worst-case complexity of the ordered partition search in MinCheck (Section 2).
Examples of command-line usage: The Grötzsch graph: triangle-free, non-3-colorable, 11 vertices: python -m pysms.graph_builder -v 11 --ck-free 3 --min-chromatic-number 4
python -m pysms.graph_builder -v 7 --ck-free 3 --all-graphs
python -m pysms.graph_builder -v 12 --diam2-critical --all-graphs python -m pysms.graph_builder -v 13 --ramsey 3 5 --all-graphs
For scripting, the GraphEncodingBuilder class provides methods for common constraints and direct clause manipulation. A simple example that enumerates maximal triangle-free graphs: from pysms.graph_builder import GraphEncodingBuilder from itertools import combinations builder = GraphEncodingBuilder(7, directed=False) builder.ckFree(3) # triangle-free for i, j in combinations(builder.V, 2): # non-neighbors must have a common neighbor builder.append([-builder.var_edge(i,j)] + [builder.CNF_AND([builder.var_edge(i,k),
builder.var_edge(j,k)]) for k in builder.V if k != i and k != j]) builder.solve(allGraphs=True)
The smsg solver can also be invoked directly with DIMACS input. Key arguments include -v for vertex count, –all-graphs for enumeration, –cutoff to limit minimality check time, and –dimacs FILE to read constraints from a file. For proof generation (Section 3.3), the solver supports outputting nc-certificates for symmetry-breaking clauses and can be configured to enable DRAT proof logging for subsequent verification. For large-scale computations, SMS supports cube-and-conquer parallelization [23] via –simple-assignment-cutoff for problem decomposition and –cube-file with –cube-line for solving individual cubes.
SAT Modulo Symmetries provides a general and efective framework for certified combinatorial search. By integrating dynamic symmetry breaking directly into the search process of a CDCL SAT solver, it avoids the exhaustive enumeration of generate-and-test methods and overcomes the incompleteness of static symmetry breaking. The core mechanism relies on testing the canonicity of partially defined objects and learning clauses to prune non-canonical branches of the search tree.
The framework’s adaptability has been demonstrated through its successful application to a wide range of problems involving graphs, hypergraphs, and matroids. Furthermore, the extension to CoCertificate Learning enables the eficient handling of problems with coNP properties. By producing verifiable certificates for both the SAT search and the symmetry breaking, SMS contributes to the growing field of computer-assisted mathematical discovery. The source code and documentation for the framework are publicly available, providing researchers with a tool to tackle other open problems in combinatorics and beyond.
The author acknowledges support from the Austrian Science Fund (FWF), project 10.55776/P36688.
During the preparation of this work, the authors used Grammarly in order to: Grammar and spelling check, paraphrase and reword. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. - Leibniz-Zentrum für Informatik, 2023, pp. 13:1–13:17. doi:10.4230/LIPICS.SAT.2023.13. [16] M. Kirchweger, M. Scheucher, S. Szeider, A SAT attack on Rota’s basis conjecture, in: K. S. Meel, O. Strichman (Eds.), 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, Schloss Dagstuhl - LeibnizZentrum für Informatik, 2022, pp. 4:1–4:18. doi:10.4230/LIPICS.SAT.2022.4. [17] D. E. Knuth, The art of computer programming. Vol. 4B. Combinatorial algorithms. Part 2, Addison
Wesley, Upper Saddle River, NJ, 2023. [18] T. Zhang, T. Peitl, S. Szeider, Small unsatisfiable k-CNFs with bounded literal occurrence, in: S. Chakraborty, J. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, August 21-24, 2024, Pune, India, volume 305 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, pp. 31:1–31:22. doi:10.4230/LIPICS.SAT. 2024.31. [19] Z. Li, C. Bright, V. Ganesh, A SAT solver and computer algebra attack on the minimum Kochen– Specker problem, in: Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, February 20-27, 2024, Vancouver, Canada, AAAI Press, 2024, pp. 23130–23131. Student Abstract. [20] M. Kirchweger, S. Szeider, Computing small rainbow cycle numbers with SAT modulo symmetries (short paper), in: P. Shaw (Ed.), 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, September 2-6, 2024, Girona, Spain, volume 307 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, pp. 37:1–37:11. doi:10.4230/LIPICS.
CP.2024.37. [21] K. Fazekas, A. Niemetz, M. Preiner, M. Kirchweger, S. Szeider, A. Biere, IPASIR-UP: user propagators for CDCL, in: M. Mahajan, F. Slivovsky (Eds.), 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, pp. 8:1–8:13. doi:10.4230/LIPICS.
SAT.2023.8. [22] DIMACS, The second DIMACS implementation challenge: 1992-1993. NP hard problems: Maximum clique, graph coloring, and satisfiability, 1992. http://dimacs.rutgers.edu/Challenges. [23] M. Heule, O. Kullmann, S. Wieringa, A. Biere, Cube and conquer: Guiding CDCL SAT solvers by lookaheads, in: K. Eder, J. Lourenço, O. Shehory (Eds.), Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers, volume 7261 of Lecture Notes in Computer Science, Springer, 2011, pp. 50–65. doi:10.1007/978-3-642-34188-5_8.