This paper presents AlphaMapleSAT, a new Cube-and-Conquer (CnC) SAT solving method based on Monte Carlo Tree Search (MCTS), designed to efficiently solve complex combinatorial problems. The authors highlight that despite the success of CnC solvers, the lookahead cubing techniques used have not seen substantial developments in recent years. AlphaMapleSAT addresses this by implementing a deductively-driven MCTS-based lookahead cubing technique, which allows for a more in-depth heuristic search for effective cubes while maintaining low cubing costs. The paper includes a comparative analysis of AlphaMapleSAT and the March CnC solver on challenging combinatorial problems, with results showing significant speed improvements.
Publication date: 24 Jan 2024
Project Page: arXiv:2401.13770v1
Paper: https://arxiv.org/pdf/2401.13770
