我正在尝试使用 Z3 (Python) 解决包含线性整数模理论的 SMT 问题。该问题类似于 Knuth 的可满足性书第 14f 页上的“学习布尔函数”示例。我的问题有一组布尔值公式（数百个），每个公式包含要求解的同一组未知整数和布尔变量（数十个），优化目标是最大化真实公式的数量作为这些公式的函数未知数。我正在努力提高解决问题的速度。这些公式包含混合布尔变量，其表达式如 (x <= const) or (x1 + x2 <= const) or (x == x1 + x2) for integers x, x1, x2, const.
从实验中我了解到：（1）使用 z3.Solver() 在决策问题上使用二分法（反复求解目标函数 >= 给定常数）似乎比直接使用 z3.Optimize() 快得多； (2) 使用“dt2bv”策略似乎可以大大提高速度。然而，解决一个大问题仍然需要数小时或数天的运行时间。
Z3 看起来有超过 100 种策略，总共超过 9000 个选项，尽管其中大部分似乎都分配给非常专业的问题类型。任何关于在哪里寻找使运行速度更快的帮助将不胜感激。如果有帮助的话，我很乐意发布示例运行的诊断输出。预先感谢您的回复。
恐怕没有一刀切的“建议”。您可以在 stack-overflow 中搜索许多问题，询问如何提高 z3 的速度，如果可能的话，答案总是“非常针对特定问题”。
你正在做的事情，即尝试不同的想法/选择是正确的方法。请注意，虽然 z3 有大量策略，但大多数都不适用。不幸的是，这些策略的记录非常少，如果有的话。
此外，您发现自己的“二分搜索”之类的实现比优化器本身的性能更好也就不足为奇了。不幸的是，z3 中的优化器实现并没有受到太多关注，特别是它不是增量的。因此，如果您发现实施自己的搜索效果更好，那么一定要这样做。或者，您可以查看OptiMathSat。它使用不同的优化方式，并且可能在此特定问题上表现更好。 （我并不是说它会；我只是说值得一试。）