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接口没有这样的方法（？）。至少现在我可以获得上限和相应的模型（代价是不必要的计算，我猜测）。

- Emilien

---

以下是使用C++ API的相同问题：Z3：C++中优化超时 - Douglas B. Staple

Answer 1

Z3可以找到满足硬约束的解，并记录目标函数和软约束的当前值。如果您要求一个模型，它将返回最后找到的模型（具有迄今为止最佳目标值的最后一个模型）。maxres策略主要改善软约束的下限（例如，任何解的成本必须至少为xx），并在可能的情况下改善上限（可选解的成本最多为yy）。下限除了缩小可能最优值的范围外，没有太多信息。当超时时，上限是可用的。您可以尝试其他策略，例如称为“wmax”的策略，它执行分支和修剪。通常，maxres表现更好，但根据问题，您可能会更喜欢使用wmax来改善上限。我没有一个模式可以让您获得模型流。原则上是可能的，但需要一些（不平凡的）重新组织。对于Pareto前沿，您可以通过连续调用Optimize.check()来获取连续的前沿。

- Nikolaj Bjorner

---

谢谢您的回答，我无法进行编辑，但您可能是指最优而不是可选。我不确定如何使用wmax策略代替maxres策略。我尝试过set_option("opt.maxres.wmax", True)，但没有看到任何显着的变化（opt.maxres日志相同）。 - Emilien

我设法更改了模型，然后使用optsmt代替。根据日志，它能够找到更好的上限。然而，当超时时，返回的模型并不是具有最佳值的模型（目标值与我使用objective.upper访问的值不同）。您知道我如何获取相应的模型吗？ - Emilien