Abstract
SAT modulo Symmetries (SMS) is a framework for the exhaustive isomorph-free generation of combinatorial objects with a prescribed property. SMS relies on the tight integration of a CDCL SAT solver with a custom dynamic symmetry-breaking algorithm that iteratively refines an ordered partition of the generated object's elements. SMS supports the generation of DRAT proofs and thus provides an additional layer of confidence in the obtained results. This talk will discuss the basic concepts of SMS and review some of its applications, including extremal graph problems like planar Turán numbers, the Earth-Moon coloring problem, Rota's matroid basis conjecture, and the Erdős-Faber-Lovász conjecture on hypergraphs.
Joint work with Katalin Fazekas, Markus Kirchweger
Tomas Peitl, and Manfred Scheucher.