Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor them 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 approaches 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 6 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.

翻译：现代SMT求解器（如Z3）支持用户可调控的策略，使用户能够针对其特定实例集定制求解策略，从而显著提升其应用场景下的求解器性能。然而，这种策略定制方法面临重大挑战：为某类SMT实例手动设计优化策略对求解器开发者和用户而言仍是复杂且艰巨的任务。本文通过一种基于蒙特卡洛树搜索的新型方法，解决自动SMT策略合成问题。该方法将策略合成视为序列决策过程，其搜索树对应于策略空间，并利用MCTS探索这一广阔空间。实现低开销下有效策略识别的关键创新在于分层与分阶段MCTS搜索的思想。这些新型方法能够更深入高效地探索策略空间，从而合成出比现有一流SMT求解器默认策略更高效的策略。我们将所提方法命名为Z3alpha，并将其作为Z3 SMT求解器的组成部分。在6种重要SMT逻辑上的大量评估表明，Z3alpha在大多数基准测试中展现出优于当前一流合成工具FastSMT、默认Z3求解器以及CVC5求解器的性能。值得注意的是，在一个具有挑战性的QF_BV基准测试集上，Z3alpha比Z3 SMT求解器中的默认策略多解决了42.7%的实例。