Smart Cubing for Graph Search: A Comparative Study
Markus Kirchweger, Hai Xia, Tom\'a\v{s} Peitl, Stefan Szeider

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsWeb Data Mining and Analysis · Data Management and Algorithms · Advanced Database Systems and Queries
