  This paper introduces AlphaMapleSAT, a novel Monte Carlo Tree Search (MCTS)
based Cube-and-Conquer (CnC) SAT solving method aimed at efficiently solving
challenging combinatorial problems. Despite the tremendous success of CnC
solvers in solving a variety of hard combinatorial problems, the lookahead
cubing techniques at the heart of CnC have not evolved much for many years.
Part of the reason is the sheer difficulty of coming up with new cubing
techniques that are both low-cost and effective in partitioning input formulas
into sub-formulas, such that the overall runtime is minimized.
  Lookahead cubing techniques used by current state-of-the-art CnC solvers,
such as March, keep their cubing costs low by constraining the search for the
optimal splitting variables. By contrast, our key innovation is a
deductively-driven MCTS-based lookahead cubing technique, that performs a
deeper heuristic search to find effective cubes, while keeping the cubing cost
low. We perform an extensive comparison of AlphaMapleSAT against the March CnC
solver on challenging combinatorial problems such as the minimum Kochen-Specker
and Ramsey problems. We also perform ablation studies to verify the efficacy of
the MCTS heuristic search for the cubing problem. Results show up to 2.3x
speedup in parallel (and up to 27x in sequential) elapsed real time.
