AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems

TL;DR

Alpha-MapleSAT introduces a novel MCTS-based cubing strategy for Cube-and-Conquer SAT solving that uses solver-derived deductive rewards to guide splits. By treating cubing as a tree MDP and applying a PUCT-guided search with propagation-rate rewards, it generates higher-quality cubes with lower overhead than greedy lookahead cubing. Empirical results on the minimum Kochen–Specker problem, the Murty–Simon Conjecture, and Ramsey problems show speedups up to 7.57x in elapsed time on 128 cores, with improved cube distributions and parallel scalability observed across both SAT+CAS and SMS conquering pipelines. The work demonstrates that deductively guided MCTS can significantly enhance hard combinatorial SAT solving and suggests avenues for future optimization and learning-enhanced variants.

Abstract

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.

Figures (3)

• Figure 1: Distribution of per-cube CPU solving times for the KS order 21 instance with SAT+CAS on 128 cores, comparing march and Alpha-MapleSAT across different variable cutoffs (VC). The figure also reports the number of cubes, along with mean and median cube solving times.
• Figure 2: Number of hard cubes (solving time $>5000$s) and cumulative time spent on these cubes for the KS order 21 instance with SAT+CAS on 128 cores. Alpha-MapleSAT generates significantly fewer hard cubes and spends substantially less time on them than march.
• Figure 3: Parallel scaling behavior on the KS order 21 instance with SAT+CAS. Total CPU time is shown as a function of the number of cores for different variable cutoffs. Alpha-MapleSAT scales consistently with increasing core counts.

Theorems & Definitions (6)

• Definition 1: Cube
• Definition 2: Propagation rate
• Definition 3: Lookahead heuristics
• Definition 4: Cubing problem
• Definition 5: Splitting or cubing tree
• Definition 6: Cubing solver