如何检查 Z3 优化问题的进度 [英] How to check progress for Z3 optimization problem

问题描述

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

I have a problem which I code up in an smt-lib file for input into Z3. There are many constraints, but really, I am interested in minimizing one variable:

        (minimize totalCost)
        (check-sat)

求解器运行了好几个小时.比我简单地使用断言将 totalCost 设置为低于某个值并运行 check-sat 的时间要长得多.有什么方法可以让 Z3 定期打印出它为 totalCost 实现的最低值，以及所有变量值来实现它?那会很有帮助.提前致谢！

The solver runs, and runs, for hours. Much longer than if I were to simply use an assert to set totalCost below some value and run check-sat. Is there any way to get Z3 to periodically print out the lowest value it has achieved for totalCost, along with all the variable values to achieve that? That would be very helpful. Thanks in advance!

推荐答案

如果您想坚持使用优化求解器，那么查看 Patrick 描述的详细模式是最好的选择.当然，输出可能难以理解，甚至可能没有您需要的所有数据.如果您深入研究，您可以检测"z3 源代码以打印出更多内容.但这需要做更多的工作，需要研究源代码.

Looking at the verbose mode as Patrick described is your best bet if you want to stick to the optimizing solver. Of course, the output might be hard to understand and may not even have all the data you need. You can "instrument" z3 source code to print out more if you dig deep into it. But that's a lot more work and would need studying the source code.

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

But it occurs to me that z3 is doing quite well with your constraints, it's the optimization engine that slows down? That's not surprising, as the optimizing solver is not as performant as the regular solver for obvious reasons. If you suspect this is the case, you might want to optimize by doing an outer loop: Do a check-sat, get the value of totalCost, then ask again but add the extra constraint that totalCost is less than the current value provided. This can quickly converge for certain problems: If the solution space is small enough and you use many different theories, this technique can outperform the optimizing solver. You can also implement a "binary" search of sorts: For instance, if the solver gives you a solution with cost 100, you can ask if there's one with cost less than 50; if sat, you'd then ask for 25, if unsat, you'd ask for 75. Depending on your problem, this can be very effective.

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

Note that if you implement the above trick, you can also use the solver in the incremental mode, and it would re-use all the lemmas it learned from before. The optimizing solver itself is not incremental, so that's another advantage of the looping technique. On the other hand, if there are too many solutions to your constraints, or if you don't have a global minimum, then the looping technique can run forever: So you probably want to watch for the loop-count and stop after a certain threshold.

这篇关于如何检查 Z3 优化问题的进度的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！