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

edit：在 opt.maxres 日志中，上限从不缩小。

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

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

Answer 1

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

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