Smart Cubing for Graph Search: A Comparative Study

TL;DR

This paper evaluates cube-and-conquer strategies for SAT solvers with dynamic propagators, focusing on symmetry-breaking in graph problems, and demonstrates significant speedups through optimized cubing and parameter tuning.

Contribution

It offers a comprehensive empirical analysis of cubing strategies for propagator-based SAT solving, introducing new insights and optimization techniques.

Findings

Speedups of 2-3x from improved cubing and tuning

Additional 1.5-2x speedup on harder instances

Effective strategies for propagator-based SAT solving

Abstract

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.