面向 SMT 策略合成的分层分阶段蒙特卡洛树搜索

现代 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% 的实例。