z3 - Can I get a solution using "timeout" when using Optimize.minimize()?

Question

I'm trying to minimize a variable, but z3 takes to long in order to give me a solution.

And I would like to know if it's possible to get a solution when timeout gets triggered.

If yes how can i do that?

Thx in advance!

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，我展示了如何在 unit-test 中检索最优值和相应模型的最新近似值timeout.py。