使用 Optimize.minimize() 时，我可以使用"timeout"获得解决方案吗？

Question

我正在尝试最小化一个变量，但是 z3 需要很长时间才能给我一个解决方案。

我想知道在触发超时时是否有可能获得解决方案。

如果是，我该怎么做？

提前感谢！

Answer 1

如果您所说的"解决方案">是指最优值的最新近似值，那么只要所使用的优化算法在此过程中找到任何中间解决方案，您就可以检索它。(一些优化算法 - 例如，maxres - 找不到任何中间解决方案(。

例：

import z3
o = z3.Optimize()
o.add(...very hard problem...)
cf = z3.Int('cf')
o.add(cf = ...)
obj = o.minimize(cf)
o.set(timeout=...)
res = o.check()
print(res)
print(obj.upper())

即使由于超时而res = unknown，objective 实例也包含z3在超时之前找到的最佳值的最新近似值。

不幸的是，我不确定是否也可以使用 o.model()(或任何其他方法(检索相应的次优模型。

---

对于OptiMathSAT，我展示了如何在单元测试timeout.py中检索最佳值和相应模型的最新近似值。