# Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 46 references that are in the map.
- First posted on arXiv 30 Jan 2024.

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

- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Symbolic Physics Learner: Discovering governing equations via Monte Carlo tree search](https://mlsanity.com/paper/2205.13134/) (2022)
- [Measuring the Size of Large No-Limit Poker Games](https://mlsanity.com/paper/1302.7008/) (2013)
- [Finding Backdoors to Integer Programs: A Monte Carlo Tree Search Framework](https://mlsanity.com/paper/2110.08423/) (2021)
- [An SMT Solver for Regular Expressions and Linear Arithmetic over String Length](https://mlsanity.com/paper/2010.07253/) (2020)
- [AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems](https://mlsanity.com/paper/2401.13770/) (2024)

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

- [SMT(LIA) Sampling with High Diversity](https://mlsanity.com/paper/2503.04782/) (2025)
- [Breaking the Data Barrier in Learning Symbolic Computation: A Case Study on Variable Ordering Suggestion for Cylindrical Algebraic Decomposition](https://mlsanity.com/paper/2601.13731/) (2026)
- [Learning Splitting Heuristics for Parallel String Solvers](https://mlsanity.com/paper/2606.20656/) (2026)

## Abstract (arXiv)

Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategies for their unique set of instances, thus dramatically enhancing solver performance for their use case. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike. In this paper, we address this problem of automatic SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42.7% more instances than the default strategy in the Z3 SMT solver.