Smart Cubing for Graph Search: A Comparative Study

TL;DR

This study adapts cube-and-conquer for SAT solving with propagators by SMS, addressing the challenge that dynamic, learned constraints complicate parallel partitioning. The authors propose a prerun-enriched encoding $F^{*}$ and evaluate multiple cubing strategies (CDCL-cutoff, CaDiCaL with look-ahead, and March_cu) alongside a final conquering solver optimized via SMAC3 and LLM-assisted scoring. Across three graph-centric benchmarks, prerun+cubing delivers 2x–3x speedups, with parameter tuning contributing an additional 1.5x–2x, especially on harder instances. The results demonstrate that carefully handling dynamically learned constraints yields substantial improvements in parallel SAT solving, and point to future directions in automated configuration and LLM-guided scoring to further enhance performance.

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.

Figures (2)

• Figure 1: The parameters ranking of CaDiCaL parameters. $10$ means a very poor rank, and that is the reason why different parameters can sometimes get the same rank.
• Figure 2: The total time to solve all cubes grouped by cube hardness. For each benchmark we compare default and march-based cubing and Def and Tun conquering solver. The height of a bar between $x_0$ and $x_1$ is the total amount of time needed to solve the cubes which took between $x_0$ and $x_1$ minutes. The rightmost bar collects all remaining cubes. The total area of each chart is proportional to the total solving time reported in Table \ref{['table:default-vs-tuned']}; all four charts for one problem use the same unit of area, and are thus pairwise comparable.