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.

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