我尝试使用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接口没有这样的方法(?)。至少现在我可以获得上限和相应的模型(代价是不必要的计算,我猜测)。