优化带约束学习的图搜索求解，提升大规模组合问题求解效率。
Smart Cubing for Graph Search: A Comparative Study
- 采用分而治之策略，结合预运行收集约束与多种分块方法。
- 在硬实例上实现2-3倍加速，复杂问题再提速1.5-2倍。
- 适用于需要对称性剪枝的组合优化场景，如图同构判定。
并行的立方体-征服法是扩展SAT求解器以应对难题的关键方法。尽管该方法在纯SAT问题中已成功应用于解决毕达哥拉斯三元组猜想，但将其应用于引入传播器的SAT求解器时面临独特挑战，因为传播器在搜索过程中动态学习约束。本文以SAT模对称性（SMS）为主要测试案例，其中对称性破缺传播器通过学习约束消除同构图，从而缩小搜索空间。通过超过10,000个CPU小时的系统性实验，我们评估了三种经典组合问题上的多种立方体-征服变体。方法包括预运行阶段收集学习约束、不同分块策略及基于算法配置和大模型生成建议的参数调优。全面的实证分析揭示了面向传播器型SAT求解的有效分块策略，最佳方法通过改进分块与参数调优实现2-3倍加速，在更难实例上额外获得1.5-2倍提升。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。