【发布时间】：2019-03-26 18:23:32
【问题描述】：
我正在尝试最小化一个变量，但 z3 需要很长时间才能给我一个解决方案。
我想知道当超时被触发时是否有可能得到解决方案。
如果是，我该怎么做？
提前谢谢！
【问题讨论】：
标签： z3 z3py optimathsat
【发布时间】：2019-03-26 18:23:32
【问题描述】：
如果 “解决方案” 是指最优值的最新近似值，那么您可能能够检索到它，前提是所使用的优化算法可以找到任何沿途的中间解决方案。 （一些优化算法——比如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 中检索最优值的最新近似值和对应模型。
【讨论】：
-
感谢您的帮助！但我得到负无穷大（-1*oo）你知道为什么吗？
-
我正在尝试最小化
-
另一个问题：我可以不使用超时退出，而是使用 if 条件吗？如果是，我该怎么做？
-
我猜这是下限 -- 如果 minimeze 低于某个限制退出求解器
-
@AndreOliveira 在最小化的情况下，
lower在不满足的二分搜索步骤上更新，upper在可满足的线性/二分搜索步骤上更新，所以你应该检查obj.upper()的值。我在z3的 API 中没有找到任何可以执行您询问的其他事情的内容。使用OptiMathSAT，使用选项opt.abort_interval或选项opt.abort_tolerance，或编写自定义的msat_termination_test回调函数，这将非常简单。