Co-Certificate Learning with SAT Modulo Symmetries

SAT modulo symmetries (SMS) is a recently proposed framework that brings efficient symmetry breaking to conflict-driven (CDCL) SAT solvers and has achieved state-of-the-art results on several symmetry-rich combinatorial search problems, enumerating or proving the non-existence of graphs, planar graphs, directed graphs, and matroids with particular properties [Kirchweger and Szeider, 2021; Kirchweger et al., 2022, 2023b]. In this paper, we propose to extend SMS to a class of problems that do not admit a succinct SAT encoding because they involve quantifier alternation: where we are asked to find a combinatorial object (the existential part) that has some co-NP-complete property (the universal part, stated as'all candidate polynomial-size witnesses fail'). We call such problems alternating search problems; a simple concrete example of an alternating search problem is the well-studied question posed by Erdős [1967], of finding a smallest triangle-free graph that is not properly k-colorable, for a fixed k 3. Encoding the non-k-colorability property for k 3 into a family of polynomially sized propositional formulas is impossible unless NP = co-NP, since checking k-colorability is NP-complete [Karp, 1972]. SMS has some advantages over alternative methods such as isomorphism-free exhaustive enumeration by canonical construction path [McKay, 1998] as implemented in tools like Nauty [McKay and Piperno, 2014], or different symmetry-breaking methods for SAT. The former can very efficiently generate all objects of a given order, but is very difficult to integrate with complex constraints and learning, while the latter is either intractable (full'static' symmetry breaking [Codish et al., 2016; Itzhakov and Codish, 2015], which requires constraints of exponential size), or ineffective (partial static symmetry breaking [Codish et al., 2019]).