This paper introduces AlphaMapleSAT, a Cube-and-Conquer (CnC) parallel SAT solver that integrates Monte Carlo Tree Search (MCTS) with deductive feedback to efficiently solve challenging combinatorial SAT problems. Traditional lookahead cubing methods, used by solvers such as March, limit their search depth to reduce overhead often resulting in suboptimal partitions. By contrast, AlphaMapleSAT performs a deeper MCTS search guided by deductive rewards from SAT solvers. This approach enables informed exploration of the cubing space while keeping cubing costs low. We demonstrate the efficacy of our technique via extensive evaluations against the widely used and established March cubing solver on three well-known challenging combinatorial benchmarks, including the minimum Kochen-Specker (KS) problem from quantum mechanics, the Murty-Simon Conjecture, and the Ramsey problems from extremal graph theory. We compare AlphaMapleSAT against March using different types of conquering solvers such as SAT Modulo Symmetries (SMS) and SAT+CAS, both built on top of the CaDiCaL SAT solver. We show that in all cases, there is a speedup in elapsed real time (wall clock time) ranging from 1.61x to 7.57x on a 128 core machine for the above-mentioned problems. We also perform cube-level and parallel scaling analysis over 32, 64, and 128 cores, which shows that AlphaMapleSAT outperforms March on all these settings. Our results show that deductively-guided MCTS search technique for cubing in CnC solvers can significantly outperform March on hard combinatorial problems.

翻译：本文介绍了AlphaMapleSAT，一种立方体-征服（CnC）并行SAT求解器，它将蒙特卡洛树搜索（MCTS）与演绎反馈相结合，以高效求解具有挑战性的组合SAT问题。传统的前瞻立方化方法（如March求解器所采用）将其搜索深度限制在较低水平以减少开销，但这常常导致次优的分区划分。相比之下，AlphaMapleSAT在SAT求解器提供的演绎奖励引导下，执行更深度的MCTS搜索。这种方法能够在保持立方化成本较低的同时，对立方化空间进行有指导的探索。我们通过在三个著名的困难组合基准测试（包括来自量子力学的最小Kochen-Specker（KS）问题、Murty-Simon猜想以及来自极值图论的Ramsey问题）上，与广泛使用且成熟的March立方化求解器进行广泛评估，证明了我们技术的有效性。我们使用不同类型的征服求解器（如基于CaDiCaL SAT求解器构建的SAT模对称性（SMS）和SAT+CAS）来比较AlphaMapleSAT与March。结果表明，在上述问题上，使用128核机器时，实际运行时间（挂钟时间）的加速比在1.61倍到7.57倍之间。我们还对32、64和128核进行了立方体级别和并行扩展性分析，表明AlphaMapleSAT在所有配置下均优于March。我们的结果表明，在CnC求解器中用于立方化的演绎引导MCTS搜索技术，在处理困难组合问题时能够显著超越March。