Z3 是否支持优化问题 [英] Does Z3 have support for optimization problems

问题描述

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

I saw in a previous post from last August that Z3 did not support optimizations. However it also stated that the developers are planning to add such support.

我在消息来源中找不到任何迹象表明这已经发生了.

I could not find anything in the source to suggest this has happened.

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

Can anyone tell me if my assumption that there is no support is correct or was it added but I somehow missed it?

谢谢，欧玛

推荐答案

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

If your optimization has an integer valued objective function, one approach that works reasonably well is to run a binary search for the optimal value. Suppose you're solving the set of constraints C(x,y,z), maximizing the objective function f(x,y,z).

1. 找到 (x0, y0, z0) 到 C(x,y,z) 的任意解.
2. 计算f0 = f(x0, y0, z0).这将是您的第一个下限.
3. 只要您不知道目标值的任何上限，请尝试解决约束 C(x,y,z) ∧ f(x,y,z) >2 * L，其中 L 是您的最佳下限(最初是 f0，然后是您认为更好的下限).
4. 一旦你有了上限和下限，应用二分搜索:solve C(x,y,z) ∧ 2 * f(x,y,z) >(U - L).如果公式可满足，您可以使用模型计算新的下限.如果是不可满足的，(U - L)/2 是一个新的上界.

1. Find an arbitrary solution (x0, y0, z0) to C(x,y,z).
2. Compute f0 = f(x0, y0, z0). This will be your first lower bound.
3. As long as you don't know any upper-bound on the objective value, try to solve the constraints C(x,y,z) ∧ f(x,y,z) > 2 * L, where L is your best lower bound (initially, f0, then whatever you found that was better).
4. Once you have both an upper and a lower bound, apply binary search: solve C(x,y,z) ∧ 2 * f(x,y,z) > (U - L). If the formula is satisfiable, you can compute a new lower bound using the model. If it is unsatisfiable, (U - L) / 2 is a new upper-bound.

如果您的问题不承认最大值，则步骤 3. 不会终止，因此如果您不确定它是否存在，您可能需要对其进行绑定.

Step 3. will not terminate if your problem does not admit a maximum, so you may want to bound it if you are not sure it does.

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

You should of course use push and pop to solve the succession of problems incrementally. You'll additionally need the ability to extract models for intermediate steps and to evaluate f on them.

我们在 Kaplan 的工作中使用了这种方法并取得了合理的成功.

We have used this approach in our work on Kaplan with reasonable success.

这篇关于Z3 是否支持优化问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！