我在去年 8 月的一篇文章中看到 Z3 不支持优化。然而，它也表示开发人员正计划添加此类支持。
我在源代码中找不到任何东西表明这已经发生了。
谁能告诉我我关于没有支持的假设是正确的还是添加了但我不知何故错过了它？
谢谢， 奥马尔
问问题
1258 次
2 回答
3
如果您的优化具有整数值目标函数，则一种效果相当好的方法是运行二进制搜索以获得最佳值。假设您正在求解一组约束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 步将不会终止，因此如果您不确定它是否存在，您可能需要绑定它。
您当然应该使用push和pop逐步解决一系列问题。您还需要能够为中间步骤提取模型并对其进行评估f。
我们在Kaplan的工作中使用了这种方法并取得了相当大的成功。
于 2013-06-21T14:03:16.797 回答
1
Z3 目前不支持优化。这在 TODO 列表中，但尚未实施。以下幻灯片描述了将在 Z3 中使用的方法：
用于计算无穷小的库已经实现，可在unstable（正在进行的工作）分支中使用，并在rise4fun在线提供。
于 2013-06-20T23:43:54.843 回答