SAT Modulo Symmetries: A Survey

Abstract

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 offer an alternative, but they require effective 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.