optimization - z3 最小化和超时

Question

我尝试使用 z3 求解器来解决最小化问题。我试图让一个超时，并返回迄今为止最好的解决方案。我使用 python API 和超时选项“smt.timeout”

set_option("smt.timeout", 1000) # 1s timeout

这实际上在大约 1 秒后超时。然而，较大的超时不会提供较小的目标。我最终打开了详细程度

set_option("verbose", 2)

而且我认为 z3 会连续评估我的目标的较大值，直到问题得到满足:

(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...

因此，我有两个问题:

我是否可以相反地告诉 z3 从上限开始，并为我的目标函数连续返回具有较小值的模型(就像例如 Minizinc 注释 indomain_max http://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html )

看起来求解器仍然返回了我的问题的一个令人满意的实例。它是如何被发现的？如果它试图连续评估我的目标的较大值，那么当超时发生时它应该还没有找到可满足的实例...

编辑 :在 opt.maxres 日志中，上限永远不会缩小。

作为记录，我在 opt_params.pyg 的源代码中找到了更详细的选项描述。

编辑 抱歉打扰了，我最近又开始研究这个了。无论如何，我认为这可能对其他人有用。我发现我实际上必须调用 Optimize.upper方法来获得上界，而模型仍然不是这个上界对应的模型。我已经能够将它添加为一个新的约束，并调用一个求解器(没有优化，只是 SAT)，但这可能不是最好的主意。通过阅读 this我觉得我应该调用 Optimize.update_upper求解器超时后，但python接口(interface)没有这样的方法(？)。至少我现在可以得到上限和相应的模型(我猜是以不必要的计算为代价的)。

Answer 1

Z3 找到硬约束的解决方案并记录目标和软约束的当前值。如果您要求模型，则返回找到的最后一个模型(迄今为止目标值最高的最后一个模型)。 maxres 策略主要改进软约束的下限(例如，任何解决方案的成本必须至少为 xx)，并尽可能提高上限(可选解决方案的成本最多为 yy)。除了缩小可能的最佳值的范围之外，下限不会告诉您太多。超时时可以使用上限。
您可以尝试其他策略之一，例如称为“wmax”的策略，它
执行分支和修剪。通常 maxres 的效果要好得多，但您可能对 wmax 有更好的经验(取决于问题)以提高上限。

我没有获得模型流的模式。原则上这是可能的，但需要进行一些(非平凡的)重组。对于帕累托前沿，您可以连续调用 Optimize.check() 以获得连续的前沿。