Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

TL;DR

This work tackles the problem of automatically synthesizing SMT solver strategies to boost performance on user-specific benchmarks. It introduces Z3alpha, an MCTS-based framework augmented with layered and staged search to efficiently navigate the vast strategy space and produce compact, effective strategies. Empirical results across six SMT logics show that Z3alpha often surpasses the default Z3 strategy, the FastSMT synthesis tool, and CVC5, including a notable 42.7% gain on challenging Sage2 benchmarks in QF_BV. The approach promises practical impact by enabling robust, interpretable strategy customization and suggests avenues for cross-solver application and broader tactic integration.

Abstract

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.

Figures (4)

• Figure 1: Context-free grammar $G$ the Z3 strategy language
• Figure 2: Illustration of the MCTS framework for strategy synthesis
• Figure 3: Comparison of the conventional MCTS and the layer-search in treating tactic parameter tuning
• Figure 4: The Staged MCTS Framework