z3 - Z3是否支持优化问题

Question

我在去年 8 月的一篇文章中看到 Z3 不支持优化。
然而，它也表示开发人员正计划添加此类支持。

我在源代码中找不到任何东西表明这已经发生了。

谁能告诉我我关于没有支持的假设是正确的还是添加了但我不知何故错过了它？

谢谢，
奥马尔

Answer 1

如果您的优化具有整数值目标函数，则一种效果相当好的方法是运行二进制搜索以获得最佳值。假设您正在求解一组约束 C(x,y,z) ，最大化目标函数f(x,y,z) .

求任意解(x0, y0, z0)至C(x,y,z) .

计算 f0 = f(x0, y0, z0) .这将是您的第一个下限。

只要您不知道目标值的任何上限，请尝试解决约束 C(x,y,z) ∧ f(x,y,z) > 2 * L , 其中 L是您最好的下限(最初是 f0 ，然后是您发现更好的下限)。

一旦你有了上限和下限，应用二分搜索:求解 C(x,y,z) ∧ 2 * f(x,y,z) > (U - L) .如果公式可以满足，您可以使用模型计算新的下限。如果不满意，(U - L) / 2是一个新的上限。

如果您的问题不接受最大值，则第 3 步将不会终止，因此如果您不确定它是否存在，您可能需要绑定(bind)它。

你当然应该使用 push和 pop逐步解决一系列问题。您还需要能够为中间步骤提取模型并评估 f在他们。

我们在 Kaplan 上的工作中使用了这种方法。以合理的成功。