Z3 优化超时 [英] Timeout for Z3 Optimize

问题描述

您如何为 z3 优化器设置超时，以便它在超时时为您提供最知名的解决方案?

How do you set a timeout for the z3 optimizer such that it will give you the best known solution when it runs out of time?

from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())

后续问题，您可以将 z3 设置为随机爬山还是始终执行完整搜索?

Follow-up question, can you set z3 to randomized hill climbing or does it always perform a complete search?

推荐答案

长回答短，你不能.这根本不是优化器的工作方式.也就是说，它没有找到解决方案，然后尝试改进它.如果您中断它或设置超时，当计时器到期时，它甚至可能没有令人满意的解决方案，更不用说以任何方式改进"了.您应该查看优化论文以了解详细信息:https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

Long answer short, you can't. That's simply not how the optimizer works. That is, it doesn't find a solution and then try to improve it. If you interrupt it or set a time-out, when the timer expires it may not even have a satisfying solution, let alone an "improved" one by any means. You should look at the optimization paper for details: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

然而，z3 确实会跟踪变量的边界，对于数值量.您可能能够提取这些值，但一般来说，您将无法知道需要从这些间隔中选择哪些值才能为整个问题提供令人满意的解决方案.请参阅此答案以进行讨论:在 Z3 上使用 SMT 约束时是否可以获得合法的范围信息

It is true, however, that z3 does keep track of bounds of variables, for numerical quantities. You might be able to extract these, though in general, you'll have no means of knowing what values out of those intervals you'd need to pick to get a satisfying solution for the overall problem. See this answer for a discussion: Is it possible to get a legit range info when using a SMT constraint with Z3

这种爬山"问题经常出现在这个论坛中.答案很简单，z3 的优化器不是这样工作的.以这种方式提出的一些先前问题:

This sort of "hill-climbing" questions come up often in this forum. And the answer is simply that's not how z3's optimizer works. Some prior questions in this manner:

• Z3 时间限制优化
• z3 最小化和超时

在 stack-overflow 中，几乎没有其他问题.搜索优化"和超时".

There are few other questions along these lines in stack-overflow. Search for "optimize" and "timeout".

这是它的理论方面.在实践中，我相信处理此类问题的最佳方法是根本不使用优化器.而是执行以下操作:

That's the theory side of it. In practice, I believe the best approach to deal with a problem of this sort is not to use the optimizer at all. Instead do the following:

1. 陈述你的问题
2. 求模型.如果没有模型，响应unsat.退出.
3. 保持当前模型为迄今为止最好的"
4. 超时?将您拥有的模型返回为迄今为止最好的".大功告成.

5. 还有时间吗?

1. State your problem
2. Ask for a model. If there's no model, respond unsat. Quit.
3. Hold on to the current model as "best-so-far"
4. Out of time? Return the model you have as "best-so-far". You are done.

5. Still have time?

5a.计算这个模型的成本".即，您试图最小化或最大化的指标.如果您将成本作为变量存储在模型中，则可以简单地从模型中查询其值.

5a. Compute the "cost" of this model. i.e., the metric you are trying to minimize or maximize. If you store the cost as a variable in your model, you can simply query its value from the model.

5b.断言一个新的约束，说成本应该低于当前模型的成本.(或者更高，如果你正在最大化.)根据你想要的花哨程度，你可能想要加倍"成本函数，或者实现某种二分搜索以更快地收敛到一个值.但这一切都取决于问题的确切细节.

5b. Assert a new constraint saying the cost should be lower than the cost of the current model. (Or higher if you are maximizing.) Depending on how fancy you want to get, you might want to "double" the cost function, or implement some sort of binary-search to converge on a value faster. But all that is really dependent on the exact details of the problem.

5c.求新型号.如果 unsat，则返回您获得的最后一个模型为最优".否则，从第 3 步开始重复.

5c. Ask for a new model. If unsat, return the last model you got as "optimal." Otherwise, repeat from step 3.

我相信这是 z3 中时间约束优化最实用的方法.它使您可以完全控制迭代的次数，并以您想要的任何方式引导搜索.(例如，您可以在每个模型中查询各种变量，并通过说给我找一个更大的 x 或一个更小的 y 等"来指导搜索，只看一个指标.)希望这是有道理的.

I believe this is the most practical approach for time-constraint optimization in z3. It gives you the full control on how many times to iterate, and guide the search in any way you want. (For instance, you can query for various variables at each model, and direct the search by saying "find me a bigger x, or a smaller y, etc., instead of looking at just one metric.) Hope that makes sense.

请注意，SMT 求解器可以像您描述的那样工作，即在超时结束时为您提供迄今为止最佳的解决方案.只是 z3 的优化器不能那样工作.对于 z3，我发现上面描述的迭代循环是这种基于超时的优化的最实用的解决方案.

Note that an SMT solver can work like you're describing, i.e., give you an optimal-so-far solution when the time-out goes off. It's just that z3's optimizer does not work that way. For z3, I found the iterative loop described as above to be the most practical solution to this sort of timeout based optimization.

你也可以看看 OptiMathSAT (http://optimathsat.disi.unitn.it/) 这可能会在这方面提供更好的设施.@Patrick Trentin 经常阅读此论坛，他是这方面的专家，他可能会单独对其使用发表意见.

You can also look at OptiMathSAT (http://optimathsat.disi.unitn.it/) which might offer better facilities in this regard. @Patrick Trentin, who reads this forum often, is an expert on that and he might opine separately regarding its usage.

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