Propositional satisfiability (SAT) solvers based on conflict-driven clause learning can solve huge instances with millions of variables and clauses [Fichte et al., 2023a]. However, for hard instances, particularly in combinatorial problems, parallelization becomes necessary. The cube-and-conquer technique has proven highly effective for such problems, most notably in resolving the Pythagorean triples conjecture [Heule et al., 2016]. In cube-and-conquer, a look-ahead solver first partitions the search space into disjoint subproblems via cubes (partial assignments), which are then solved independently by CDCL solvers. This independence enables efficient parallel solving. When encoding combinatorial problems into SAT, particularly those involving graphs, we often encounter highly symmetric search spaces. Many mutually isomorphic graphs satisfy the same constraints, but a solver needs to check only one representative, the canonical element, from each isomorphism class. Standard CDCL solvers cannot leverage these symmetries, and static symmetry breaking methods cannot break all symmetries [Codish et al., 2019]. SAT Modulo Symmetries (SMS) [Kirchweger and Szeider, 2021; Kirchweger and Szeider, 2024] addresses this limitation through dynamic symmetry breaking, using a custom propagator that learns symmetry-breaking predicates during the search.

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]).