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.

通过采用基于蒙特卡罗树搜索（MCTS）的新方法，我们解决了自动 SMT 策略合成的问题，使得 Z3alpha 相比于状态 - of-the-art 的 SMT 解析工具 FastSMT，Z3 解析器和 CVC5 解析器，在大多数基准测试中都展示了卓越的性能，尤其是在具有挑战性的 QF_BV 基准集上，Z3alpha 解决的实例比 Z3 解析器默认策略多 42.7%。

分层分阶蒙特卡洛树搜索用于 SMT 策略合成

Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis

We develop a general framework for abstracting the behavior of an agent that
operates in a nondeterministic domain, i.e., where the agent does not control
the outcome of the nondeterministic actions, based on the nondeterministic
situation calculus and the ConGolog programming language. We assume that we
have both an abstract and a concrete nondeterministic basic action theory, and
a refinement mapping which specifies how abstract actions, decomposed into
agent actions and environment reactions, are implemented by concrete ConGolog
programs. This new setting supports strategic reasoning and strategy synthesis,
by allowing us to quantify separately on agent actions and environment
reactions. We show that if the agent has a (strong FOND) plan/strategy to
achieve a goal/complete a task at the abstract level, and it can always execute
the nondeterministic abstract actions to completion at the concrete level, then
there exists a refinement of it that is a (strong FOND) plan/strategy to
achieve the refinement of the goal/task at the concrete level.

论文提出了一个基于 ConGolog 编程语言和非确定情景演算的抽象化代理行为的通用框架，在支持策略推理和策略合成的同时，实现了代理动作和环境反应的分离量化。如果代理在抽象层次有一个 (plan/strategy) 可以实现目标 / 完成任务，并且可以在具体层次始终执行非确定性的抽象行为从而实现目标 / 任务，则存在一个对具体目标 / 任务的细化的 (plan/strategy) 实现。

非确定性 Situation Calculus 动作理论的抽象 —— 扩展版

Abstraction of Nondeterministic Situation Calculus Action Theories --  Extended Version

Consumption Markov Decision Processes (CMDPs) are probabilistic
decision-making models of resource-constrained systems. In a CMDP, the
controller possesses a certain amount of a critical resource, such as electric
power. Each action of the controller can consume some amount of the resource.
Resource replenishment is only possible in special reload states, in which the
resource level can be reloaded up to the full capacity of the system. The task
of the controller is to prevent resource exhaustion, i.e. ensure that the
available amount of the resource stays non-negative, while ensuring an
additional linear-time property. We study the complexity of strategy synthesis
in consumption MDPs with almost-sure B\"uchi objectives. We show that the
problem can be solved in polynomial time. We implement our algorithm and show
that it can efficiently solve CMDPs modelling real-world scenarios.

本文研究了 Consumption Markov Decision Processes（CMDPs）中具有几乎确定的 B"uchi 对象的策略综合的复杂性，并证明了该问题可以在多项式时间内解决。 我们实施了该算法，并证明它可以有效地解决模拟真实情景的 CMDP 问题。