optimization - Z3 优化超时

Question

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

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

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

Answer 1

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

然而，对于数值量，z3 确实会跟踪变量的边界。您可能能够提取这些，但一般来说，您无法知道需要从这些间隔中选择哪些值才能为整个问题获得令人满意的解决方案。请参阅此答案进行讨论:Is it possible to get a legit range info when using a SMT constraint with Z3

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

• Z3 Time Restricted Optimization
• z3 minimization and timeout

在堆栈溢出中几乎没有其他问题。搜索“优化”和“超时”。

您最好的选择

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

1. 说出你的问题
2. 索要型号。如果没有模型，则响应 unsat。退出。
3. 将当前模型保持为“迄今为止最好的”
4. 没时间了？将您拥有的模型返回为“迄今为止最好的”。大功告成。

5. 还有时间吗？

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

   5b。断言一个新的约束，说成本应该低于当前模型的成本。 (如果您要最大化，则更高。)根据您想要获得的花哨程度，您可能希望将成本函数“加倍”，或者实现某种二进制搜索以更快地收敛到一个值。但这一切都取决于问题的具体细节。

   5c。求一个新模型。如果 unsat，则将您获得的最后一个模型返回为“最佳”。否则，从第 3 步开始重复。

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

总结

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

您还可以查看 OptiMathSAT (http://optimathsat.disi.unitn.it/)，它可能在这方面提供更好的设施。 @Patrick Trentin 经常阅读这个论坛，他是这方面的专家，他可能会就其用法单独发表意见。