z3最小化和超时 [英] z3 minimization and timeout
问题描述
我尝试将z3求解器用于最小化问题.我试图超时，并返回到目前为止最好的解决方案.我使用python API，并将超时选项"smt.timeout"与
I try to use the z3 solver for a minimization problem. I was trying to get a timeout, and return the best solution so far. I use the python API, and the timeout option "smt.timeout" with
set_option("smt.timeout", 1000) # 1s timeout
这实际上在大约1秒钟后超时.但是，较大的超时不会提供较小的目标.我最终用
This actually times out after about 1 second. However a larger timeout does not provide a smaller objective. I ended up turning on the verbosity with
set_option("verbose", 2)
我认为z3会连续评估我的目标的较大值，直到问题可以解决为止:
And I think that z3 successively evaluates larger values of my objective, until the problem is satisfiable:
(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...
因此，我有两个问题:
- Can I on contrary tell z3 to start with the upper bound, and successively return models with a smaller value for my objective function (just like for instance Minizinc annotations
indomain_maxhttp://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html) - It still looks like the solver returns a satisfiable instance of my problem. How is it found? If it's trying to evaluates larger values of my objective successively, it should not have found a satisfiable instance yet when the timeout occurs...
编辑:在opt.maxres日志中，上限从未缩小.
edit: In the opt.maxres log, the upper bound never shrinks.
出于记录目的，我在这里的源中找到了对选项的更详细的描述 opt_params.pyg
For the record, I found a more verbose description of the options in the source here opt_params.pyg
编辑很抱歉，最近我再次涉猎于此.无论如何，我认为这可能对其他人有用.我发现我实际上必须调用Optimize.upper方法才能获得上限，并且该模型仍然不是与该上限相对应的模型.我已经能够将其添加为新的约束，并调用一个求解器(没有优化，只有SAT)，但这可能不是最好的主意.通过阅读此，我觉得我应该给
Edit Sorry to bother, I've beed diving into this recently once again. Anyway I think this might be usefull to others. I've been finding that I actually have to call the Optimize.upper method in order to get the upper bound, and the model is still not the one that corresponds to this upper bound. I've been able to add it as a new constraint, and call a solver (without optimization, just SAT), but that's probably not the best idea. By reading this I feel like I should call Optimize.update_upper after the solver times out, but the python interface has no such method (?). At least I can get the upper bound, and the corresponding model now (at the cost of unneccessary computations I guess).
推荐答案
Z3查找硬约束的解决方案，并记录目标和软约束的当前值.如果您需要一个模型，则返回找到的最后一个模型(迄今为止具有最佳目标价值的模型). maxres策略主要改善软约束的下限(例如，任何解决方案的成本至少为xx)，并在可能的情况下提高上限(可选解决方案的成本至多为yy).除了缩小可能的最佳值范围之外，下限不会告诉您太多.当您超时时，上限是可用的. 您可以尝试其他策略之一，例如称为"wmax"的策略， 执行分支修剪.通常，maxres的性能要好得多，但是使用wmax改善上限时，您可能会有更好的经验(取决于问题).
Z3 finds solutions for the hard constraints and records the current values for the objectives and soft constraints. The last model that was found (the last model with the so-far best value for the objectives) is returned if you ask for a model. The maxres strategy mainly improves the lower bounds on the soft constraints (e.g., any solution must have cost at least xx) and whenever possible improves the upper bound (the optional solution has cost at most yy). The lower bounds don't tell you too much other than narrowing the range of possible optimal values. The upper bounds are available when you timeout. You could try one of the other strategies, such as the one called "wmax", which performs a branch-and-prune. Typically maxres does significantly better, but you may have better experience (depending on the problems) with wmax for improving upper bounds.
我没有一种模式可以让您获得一系列模型.从原则上讲这是可能的，但将需要进行一些(非常重要的)重组.对于帕累托前沿，您可以对Optimize.check()进行连续调用以获取连续前沿.
I don't have a mode where you get a stream of models. It is in principle possible, but it would require some (non-trivial) reorganization. For Pareto fronts you make successive invocations to Optimize.check() to get the successive fronts.
这篇关于z3最小化和超时的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
