如何检查 Z3 优化问题的进度答案

【问题标题】：How to check progress for Z3 optimization problem如何检查 Z3 优化问题的进度
【发布时间】：2020-01-18 19:58:49
【问题描述】：

我有一个问题，我在一个 smt-lib 文件中编码以输入到 Z3。有很多限制，但实际上，我对最小化一个变量很感兴趣：

        (minimize totalCost)
        (check-sat)

求解器运行了几个小时。比我简单地使用断言将 totalCost 设置为低于某个值并运行 check-sat 的时间要长得多。有没有办法让 Z3 定期打印出它为 totalCost 实现的最低值，以及实现该值的所有变量值？那将非常有帮助。提前致谢！

【问题讨论】：

标签： performance optimization z3 minimize maximize

【解决方案1】：

如果您想坚持优化求解器，最好查看 Patrick 所描述的详细模式。当然，输出可能难以理解，甚至可能没有您需要的所有数据。如果您深入研究它，您可以“检测”z3 源代码以打印出更多内容。但这需要更多的工作，并且需要研究源代码。

但我突然想到 z3 在你的约束下做得很好，是优化引擎变慢了？这并不奇怪，因为显而易见的原因，优化求解器的性能不如常规求解器。如果您怀疑是这种情况，您可能希望通过执行外循环进行优化：执行check-sat，获取totalCost 的值，然后再次询问，但添加totalCost 小于当前的额外约束提供的价值。对于某些问题，这可以快速收敛：如果解决方案空间足够小并且您使用许多不同的理论，则该技术可以胜过优化求解器。您还可以实现某种“二进制”搜索：例如，如果求解器给您一个成本为100 的解决方案，您可以询问是否有一个成本低于50 的解决方案；如果sat，那么你会要求25，如果unsat，你会要求75。根据您的问题，这可能非常有效。

请注意，如果你实现了上述技巧，你也可以在增量模式下使用求解器，它会重新使用它之前学到的所有引理。优化求解器本身不是增量的，因此这是循环技术的另一个优点。另一方面，如果您的约束有太多的解决方案，或者如果您没有全局最小值，那么循环技术可以永远运行：所以您可能希望观察循环计数并在某个特定时间后停止阈值。

【讨论】：

感谢您的回答。详细选项有助于查看进度。我希望有一种方法可以说“运行 15 分钟，然后返回“未确定”或找到的最低成本，以及必要的模型/变量分配。我将按照您的建议尝试以增量模式运行。以前，我在 maxCost
您可以给 z3 一个时间限制，但我认为它不会在超时到期时转储“当前”值。（检查-T 和-t 选项。）正如Patrick 提到的，根据约束，这样的当前值甚至可能不可用。尝试使用二分查找的增量模式；这可能是你最好的选择。

【解决方案2】：

如果您通过命令行运行 z3，您可以尝试使用选项 -v:1，这会使 OMT 求解器打印成本函数下限/上限的任何更新。

例如

~$ z3 -v:1 optimathsat/tools/release_files/examples/optimization/smtlib2_binary.smt2
...
(optsmt upper bound: 57)
(optsmt upper bound: 54)
(optsmt upper bound: 157/3)
(optsmt upper bound: 52)
(optsmt upper bound: 154/3)
(optsmt upper bound: 50)
(optsmt upper bound: 149/3)
(optsmt upper bound: 97/2)
(optsmt upper bound: 145/3)
(optsmt upper bound: 48)
(optsmt upper bound: 95/2)
(optsmt upper bound: 140/3)
(optsmt upper bound: 46)
(optsmt upper bound: 181/4)
(optsmt upper bound: 45)
(optsmt upper bound: 134/3)
(optsmt upper bound: 89/2)
(optsmt upper bound: 177/4)
(optsmt upper bound: 44)
(optsmt upper bound: 43)
(optsmt upper bound: 171/4)
(optsmt upper bound: 128/3)
(optsmt upper bound: 85/2)
(optsmt upper bound: 42)
(optsmt upper bound: 81/2)
(optsmt upper bound: 202/5)
(optsmt upper bound: 40)
(optsmt upper bound: 199/5)
(optsmt upper bound: 193/5)
(optsmt upper bound: 77/2)
(optsmt upper bound: 192/5)
(optsmt upper bound: 115/3)
(optsmt upper bound: 191/5)
(optsmt upper bound: 189/5)
(optsmt upper bound: 217/6)
(optsmt upper bound: 36)
(optsmt upper bound: 69/2)
(optsmt upper bound: 137/4)
(optsmt upper bound: 34)
(optsmt upper bound: 65/2)
(optsmt upper bound: 223/7)
(optsmt upper bound: 63/2)
(optsmt upper bound: 218/7)
(optsmt upper bound: 216/7)
(optsmt upper bound: 123/4)
(optsmt upper bound: 61/2)
(optsmt upper bound: 211/7)
(optsmt upper bound: 241/8)
(optsmt upper bound: 30)
(optsmt upper bound: 208/7)
(optsmt upper bound: 59/2)
(optsmt upper bound: 115/4)
(optsmt upper bound: 57/2)
(optsmt upper bound: 113/4)
(optsmt upper bound: 253/9)
(optsmt upper bound: 251/9)
(optsmt upper bound: 250/9)
(optsmt upper bound: 221/8)
(optsmt upper bound: 55/2)
(optsmt upper bound: 192/7)
(optsmt upper bound: 191/7)
(optsmt upper bound: 109/4)
(optsmt upper bound: 217/8)
(optsmt upper bound: 27)
sat
(objectives
 (objective 27)
)

这仅在使用的优化算法从可满足区域开始推进搜索时才有用。一些优化引擎，例如MaxRes，从不可满足（即超过最优）区域开始接近最优解，因此不提供任何部分解（但是，在某些情况下它们可能会快得多）。

【讨论】：