我尝试将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接口没有这样的方法(?)。至少我现在可以获得上限和相应的模型(我想以不必要的计算为代价)。 最佳答案
Z3查找硬约束的解决方案,并记录目标和软约束的当前值。如果您需要一个模型,则返回找到的最后一个模型(具有迄今为止目标最佳价值的最后一个模型)。 maxres策略主要改善软约束的下限(例如,任何解决方案的成本至少为xx),并在可能的情况下提高上限(可选解决方案的成本最高为yy)。除了缩小可能的最佳值范围之外,下限不会告诉您太多。超时时可以使用上限。
您可以尝试其他策略之一,例如称为“ wmax”的策略,
执行分支修剪。通常,maxres的性能要好得多,但是使用wmax改善上限时,您可能会有更好的经验(取决于问题)。
我没有一种模式可以让您获得一系列模型。从原则上讲这是可能的,但将需要进行一些(非常重要的)重组。对于帕累托前沿,您可以连续调用Optimize.check()以获得连续前沿。