我在去年八月份的一篇文章中看到Z3不支持优化。
但它也表示，开发人员正计划添加此类支持。
我在来源中找不到任何表明发生这种情况的内容。
谁能告诉我我关于没有支持的假设是否正确，或者是否已添加但我不知何故错过了它？
谢谢，
奥马尔
如果您的优化具有整数值目标函数，则一种效果相当好的方法是运行二分搜索以获得最佳值。假设您正在解决一组约束C(x,y,z)，最大化目标函数f(x,y,z).
- 找到任意解
(x0, y0, z0) to C(x,y,z).
- Compute
f0 = f(x0, y0, z0)。这将是您的第一个下限。
- 只要您不知道目标值的任何上限，就尝试解决约束
C(x,y,z) ∧ f(x,y,z) > 2 * L, where L是你的最佳下限（最初，f0，那么无论你发现什么都更好）。
- 一旦你有了上限和下限，应用二分搜索：解决
C(x,y,z) ∧ 2 * f(x,y,z) > (U - L)。如果公式可满足，您可以使用模型计算新的下限。如果还不满意的话(U - L) / 2是一个新的上限。
如果您的问题未达到最大值，则步骤 3. 将不会终止，因此如果您不确定是否可以，则可能需要对其进行限制。
你当然应该使用push and pop逐步解决一系列问题。您还需要能够提取中间步骤的模型并评估f在他们。
我们在工作中使用了这种方法Kaplan并取得合理的成功。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
