使用Optimize.minimize（）时，我可以使用“超时”获得解决方案吗？

Question

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

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

如果是的话我该怎么做？

Thx提前！

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中检索最佳值的最新近似值和相应的模型。