Smart Cubing for Graph Search: A Comparative Study
This work addresses the problem of scaling SAT solvers with propagators for researchers in combinatorial search and automated reasoning, but it is incremental as it builds on existing cube-and-conquer methods.
The paper tackled the challenge of applying cube-and-conquer methods to SAT solvers with dynamic propagators, such as SAT Modulo Symmetries, by evaluating different variants on combinatorial problems, resulting in speedups of 2-3x from improved cubing and parameter tuning, with an additional 1.5-2x improvement on harder instances.
Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers extended with propagators presents unique challenges, as these propagators learn constraints dynamically during the search. We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs. Through extensive experimentation comprising over 10,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration and LLM-generated design suggestions. The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving, with our best method achieving speedups of 2-3x from improved cubing and parameter tuning, providing an additional 1.5-2x improvement on harder instances.