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

Question

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

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

如果是，我该怎么做？

提前致谢！

Answer 1

如果"solution"指的是最优值的最新近似值，那么可能能够检索到它，前提是所使用的优化算法在此过程中找到任何中间解决方案。 （一些优化算法——例如，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, I show how to retrieve the latest approximation of the optimum value and the corresponding model in the unit-test timeout.py。

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

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

z3

z3py

optimathsat