社区最佳实践对于帮助更有效地使用软件产品很有用。我刚刚使用 Z3 求解器完成了一个小项目。以下是我学到的一些东西：
- 我的项目涉及一个优化问题：对于布尔变量的子集，最大化有多少为真。通过转换为决策问题，使用 Z3 可以更快地解决我的具体问题：设置一个基本问题来解决计数至少为某个固定数字的问题，并使用二分搜索进行迭代以找到满足的最高数字。之前已经用二分法解决过这个问题。此外，某些方法可能会减少二分步骤的数量。
- 使用Z3“策略”可以大大加快求解过程。我通过反复试验找到了很好的策略组合，部分是由策略描述指导的。 ChatGPT 在寻找合适的选择方面提供了一些帮助。一篇有趣的论文讨论了使用蒙特卡罗树搜索来定义良好的策略链。这里的分支因子很高，可能在 1000 左右，尽管这个数字有一些冗余。训练多步 MCTS 可能很昂贵，但这样做一次以获得良好的静态策略链可能是值得的。
- Z3 的优势在于其极其广泛的功能，而不仅仅是其原始计算性能。对于 Z3 团队来说，全面优化每一个可能的解决方案将是一项艰巨的任务。我检查了一些 SMT 求解器竞赛，以找到更快的代码。我尝试过的一个案例中， CVC5 的速度大约是 Z3 的两倍；我在文献中看到过类似的报道。目前我认为不值得付出转换成本来使用 CVC5。一种方法可能是使用 Z3 非常强大的战术引擎，并将生成的修改问题传递给 CVC5。
- 问题的具体表述可以对求解器的性能产生很大的影响。我已经在迭代线性求解器领域看到了这一点，例如对角矩阵缩放可以极大地帮助（共轭梯度）或损害（多重网格）求解器性能。这里同样的事情。因此，良好的“预处理”对于 SAT/SMT 求解器非常重要。人们可能希望求解器能够自动处理所有这些而无需用户干预。然而，这些强大的工具必须非常小心地使用才能发挥最大效果。
- 一般来说，人们应该将尽可能多的问题移到求解器之外，因为就可扩展性而言，求解器是帐篷中的长杆。例如，如果有一个 Z3 整数必须限制在某个范围内，并且该区间中的某些值必须被列入黑名单，那么如果可能的话，最好将所有有效值压缩到单个区间中，以便在 Z3 代码中更简单地测试有效性。
- 沿着这些思路：Z3 传播常数的策略并不完美；因此它可以帮助手动传播常量（尽管不幸的是这使代码更加混乱）。这种传播有时还可以消除不需要的约束，进一步提高性能。与此相关，Benjamin Mikek 的一些有趣的工作展示了如何使用 LLVM 代码优化器以一种与 Z3 策略互补的方式优化 SMT 问题，从而实现显着的加速（更多信息请参见此处、此处和此处）。我还没有尝试过，但看起来很有希望。
- 由于 SMT 求解器的可扩展性挑战，各种简化启发式方法来修改问题可能会有所帮助。例如：解决主问题的子问题并固定结果变量以解决问题的其余部分。或者首先解决一个更简单、更小的问题，以确定整个问题的变量预设。通过这些启发式方法，人们通常无法找到真正的全局最优值。但结果可能已经足够了。
- CPU 线程不适用于我的情况（Z3 Python、macOS）。 SAT 和 SMP 的完美并行化是一个未解决的（也许在某种意义上不能完全解决）问题。人们可以通过转换为三等分来简单地并行二分搜索，但这并不能提供完美的加速（具体来说，P 线程上的 log(P) 加速）。在某些情况下，并行二分的改进是可能的。 Armin Biere 及其同事最近的工作看起来很有希望。当我读到它时，几乎完美地加速到八个线程（至少对于某些问题）。
- Z3 的一些主要开发人员都在Stack Overflow上，并且过去一直积极回答问题。这看起来很有用。
满意度手册和各种 SAT/SMT 会议记录等资源似乎很有帮助。有关非专家从业者最佳实践的更多信息将对社区有很大帮助。如果您知道什么好的资源，请在评论中分享。
使用 Z3 SAT/SMT 求解器获得的经验教训一文首次出现在John D. Cook上。
原文： https://www.johndcook.com/blog/2025/03/17/lessons-learned-with-the-z3-sat-smt-solver/