Layered and Staged Monte Carlo Tree Search for SMT
                                Strategy Synthesis
                                Zhengyang Lu1 , Stefan Siemer2 , Piyush Jha3 , Joel Day4 , Florin Manea2 and
                                Vijay Ganesh4
                                1
                                  University of Waterloo, Canada
                                2
                                  University of Goẗtingen and CIDAS, Germany
                                3
                                  Georgia Institute of Technology, USA
                                4
                                  Loughborough University, UK


                                                                         Abstract
                                                                         Modern SMT solvers, such as Z3, offer user-controllable strategies that allow solver users the ability
                                                                         to tailor solving strategies for their unique set of instances, thus dramatically enhancing the solver
                                                                         performance for their specific use cases. 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 the problem of automated 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 𝑄𝐹 _𝐵𝑉 benchmark set,
                                                                         Z3alpha solves 42.7% more instances than the default strategy in Z3.




                                SMT 2024: 22st International Workshop on Satisfiability Modulo Theories July 22–23, 2024, Montreal Canada
                                $ john.lu2@uwaterloo.ca (Z. Lu); stefan.siemer@cs.uni-goettingen.de (S. Siemer); piyush.jha@gatech.edu (P. Jha);
                                j.day@lboro.ac.uk (J. Day); florin.manea@informatik.uni-goettingen.de (F. Manea); vganesh@gatech.edu
                                (V. Ganesh)
                                                                       © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
                                    CEUR
                                    Workshop
                                    Proceedings
                                                  http://ceur-ws.org
                                                  ISSN 1613-0073
                                                                       CEUR Workshop Proceedings (CEUR-WS.org)




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings