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 legal range info when using a SMTconstraint with Z3

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

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

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

你最好的选择

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

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 经常阅读这个论坛，他是这方面的专家，他可能会就其用法单独发表意见。