# UNSAT Solver Synthesis via Monte Carlo Forest Search

arXiv: https://arxiv.org/abs/2211.12581 · HTML: https://mlsanity.com/paper/2211.12581/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 78 references that are in the map.
- First posted on arXiv 22 Nov 2022.

## Builds on (most cited first, 20 of 20)

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Mastering Atari, Go, Chess and Shogi by Planning with a Learned Model](https://mlsanity.com/paper/1911.08265/) (2019)
- [Machine Learning for Combinatorial Optimization: a Methodological Tour d'Horizon](https://mlsanity.com/paper/1811.06128/) (2018)
- [Exact Combinatorial Optimization with Graph Convolutional Neural Networks](https://mlsanity.com/paper/1906.01629/) (2019)
- [Solving Mixed Integer Programs Using Neural Networks](https://mlsanity.com/paper/2012.13349/) (2020)
- [Deep Models of Interactions Across Sets](https://mlsanity.com/paper/1803.02879/) (2018)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Learning to branch with Tree MDPs](https://mlsanity.com/paper/2205.11107/) (2022)
- [Reinforcement Learning for Variable Selection in a Branch and Bound Algorithm](https://mlsanity.com/paper/2005.10026/) (2020)
- [One Model, Any CSP: Graph Neural Networks as Fast Global Search Heuristics for Constraint Satisfaction](https://mlsanity.com/paper/2208.10227/) (2022)
- [Reinforcement Learning for Branch-and-Bound Optimisation using Retrospective Trajectories](https://mlsanity.com/paper/2205.14345/) (2022)
- [Deep Learning Assisted Heuristic Tree Search for the Container Pre-marshalling Problem](https://mlsanity.com/paper/1709.09972/) (2017)
- [Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning](https://mlsanity.com/paper/1807.08058/) (2018)
- [Finding Backdoors to Integer Programs: A Monte Carlo Tree Search Framework](https://mlsanity.com/paper/2110.08423/) (2021)
- [Learning Branching Heuristics for Propositional Model Counting](https://mlsanity.com/paper/2007.03204/) (2020)
- [Learning Variable Ordering Heuristics for Solving Constraint Satisfaction Problems](https://mlsanity.com/paper/1912.10762/) (2019)
- [Monte-Carlo Graph Search for AlphaZero](https://mlsanity.com/paper/2012.11045/) (2020)
- [Move Evaluation in Go Using Deep Convolutional Neural Networks](https://mlsanity.com/paper/1412.6564/) (2014)

## Built on by (most cited first, 3 of 3)

- [Learning from Algorithm Feedback: One-Shot SAT Solver Guidance with GNNs](https://mlsanity.com/paper/2505.16053/) (2025)
- [A Reinforcement Learning based Reset Policy for CDCL SAT Solvers](https://mlsanity.com/paper/2404.03753/) (2024)
- [Learning How to Cube](https://mlsanity.com/paper/2605.16632/) (2026)

## Abstract (arXiv)

We introduce Monte Carlo Forest Search (MCFS), a class of reinforcement learning (RL) algorithms for learning policies in {tree MDPs}, for which policy execution involves traversing an exponential-sized tree. Examples of such problems include proving unsatisfiability of a SAT formula; counting the number of solutions of a satisfiable SAT formula; and finding the optimal solution to a mixed-integer program. MCFS algorithms can be seen as extensions of Monte Carlo Tree Search (MCTS) to cases where, rather than finding a good path (solution) within a tree, the problem is to find a small tree within a forest of candidate trees. We instantiate and evaluate our ideas in an algorithm that we dub Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies for solving the Boolean satisfiability (SAT) problem, with the objective of achieving good average-case performance on a given distribution of unsatisfiable problem instances. Knuth Synthesis is the first RL approach to avoid the prohibitive costs of policy evaluations in an exponentially-sized tree, leveraging two key ideas: first, we estimate tree size by randomly sampling paths and measuring their lengths, drawing on an unbiased approximation due to Knuth (1975); second, we query a strong solver at a user-defined depth rather than learning a policy across the whole tree, to focus our policy search on early decisions that offer the greatest potential for reducing tree size. We matched or exceeded the performance of a strong baseline on three well-known SAT distributions, facing problems that were two orders of magnitude more challenging than those addressed in previous RL studies.