AlphaMapleSAT：一种基于MCTS的Cube-and-Conquer SAT求解器用于困难组合问题
人工智能
2026-01-21 v2 组合数学
摘要
本文介绍了 AlphaMapleSAT，这是一种 Cube-and-Conquer (CnC) 并行 SAT 求解器，它将蒙特卡洛树搜索 (MCTS) 与演绎反馈相结合，以高效解决具有挑战性的组合 SAT 问题。诸如 March 等求解器使用的传统前瞻分块方法将其搜索深度限制为以减少开销，这通常导致次优的划分。相比之下，AlphaMapleSAT 在来自 SAT 求解器的演绎奖励的引导下执行更深层的 MCTS 搜索。这种方法能够在保持较低分块成本的同时，对分块空间进行有信息的探索。我们通过在三个著名的具有挑战性的组合基准上与广泛使用且成熟的 March 分块求解器进行广泛评估，展示了我们技术的有效性，这些基准包括来自量子力学的最小 Kochen-Specker (KS) 问题、Murty-Simon 猜想以及来自极值图论的 Ramsey 问题。我们使用不同类型的征服求解器（例如 SAT Modulo Symmetries (SMS) 和 SAT+CAS）比较了 AlphaMapleSAT 与 March，这两者均构建在 CaDiCaL SAT 求解器之上。我们表明，在 128 核机器上，对于上述问题，实际流逝时间（挂钟时间）的加速比从 1.61 倍到 7.57 倍不等。我们还在 32、64 和 128 核上进行了分块级别和并行扩展性分析，这表明 AlphaMapleSAT 在所有这些设置下均优于 March。我们的结果表明，用于 CnC 求解器中分块的演绎引导 MCTS 搜索技术在困难组合问题上可以显著优于 March。
引用
@article{arxiv.2401.13770,
title = {AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems},
author = {Piyush Jha and Zhengyu Li and Zhengyang Lu and Raymond Zeng and Curtis Bright and Vijay Ganesh},
journal= {arXiv preprint arXiv:2401.13770},
year = {2026}
}
备注
Added more experiments