z3最小化和超时

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

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_maxhttp://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html）
它仍然看起来像求解器返回我的问题的可满足的实例。它是如何发现的？如果它试图先后评估大我的目标的值，它不应该发生超时时发现还没有令人满意的情况下...

编辑：在opt.maxres日志，上界永远不会收缩。

为了记录在案，我发现的选项更详细的描述在这儿为源极opt_params.pyg

编辑对不起，打扰，我已经木珠潜入这家最近的一次。无论如何，我认为这可能对其他人有用。我发现我实际上必须调用Optimize.upper方法来获得上限，并且该模型仍然不是与此上限相对应的方法。我已经能够将它添加为一个新的约束，并称为解算器（没有优化，只是SAT），但这可能不是最好的主意。通过阅读this我觉得我应该在解算器超时后调用Optimize.update_upper，但python接口没有这样的方法（？）。至少我现在可以得到上限和相应的模型（以不必要的计算为代价）。

来源

2016-02-04 Emilien

下面是使用C++ API的相同问题：[Z3：用于C++优化的超时]（https://stackoverflow.com/questions/38674049/z3-timeout-for-optimize-in-c/38680055） –

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

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

来源

2016-02-04 18:03:57

感谢你的答案，我不能编辑，但你可能意味着最佳，而不是可选。我不知道如何使用wmax策略而不是maxres策略。我尝试了'set_option（“opt.maxres.wmax”，True）'但我没有看到任何重大更改（opt.maxres日志相同）。 – Emilien

所以我设法改变模型，然后使用'optsmt'，而根据日志找到更好的上界。但是，当它超时时，返回的模型不是具有目前最佳值的那个（目标值与我可以使用'objective.upper'访问的目标值不同）。你知道我怎么能得到相应的模型？ – Emilien

z3最小化和超时

回答

相关问题