# Solving QSAT problems with neural MCTS

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 21 references that are in the map.
- First posted on arXiv 17 Jan 2021.

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

- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [Relational inductive biases, deep learning, and graph networks](https://mlsanity.com/paper/1806.01261/) (2018)
- [Gated Graph Sequence Neural Networks](https://mlsanity.com/paper/1511.05493/) (2015)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Thinking Fast and Slow with Deep Learning and Tree Search](https://mlsanity.com/paper/1705.08439/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Learning Self-Game-Play Agents for Combinatorial Optimization Problems](https://mlsanity.com/paper/1903.03674/) (2019)
- [Symmetries of Quantified Boolean Formulas](https://mlsanity.com/paper/1802.03993/) (2018)

## Abstract (arXiv)

Recent achievements from AlphaZero using self-play has shown remarkable performance on several board games. It is plausible to think that self-play, starting from zero knowledge, can gradually approximate a winning strategy for certain two-player games after an amount of training. In this paper, we try to leverage the computational power of neural Monte Carlo Tree Search (neural MCTS), the core algorithm from AlphaZero, to solve Quantified Boolean Formula Satisfaction (QSAT) problems, which are PSPACE complete. Knowing that every QSAT problem is equivalent to a QSAT game, the game outcome can be used to derive the solutions of the original QSAT problems. We propose a way to encode Quantified Boolean Formulas (QBFs) as graphs and apply a graph neural network (GNN) to embed the QBFs into the neural MCTS. After training, an off-the-shelf QSAT solver is used to evaluate the performance of the algorithm. Our result shows that, for problems within a limited size, the algorithm learns to solve the problem correctly merely from self-play.