Z3限时优化 [英] Z3 Time Restricted Optimization

问题描述

我已经看到Z3支持通过以下方式进行优化:断言软.据我了解，如果有足够的时间，Z3将报告给定SMT公式的最佳解决方案.

I have seen that Z3 supports optimization via e.g. assert-soft. From what I understood, if given sufficient time, Z3 will report the optimal solution for a given SMT formula.

但是，我很感兴趣是否有可能在有限的时间内运行Z3并报告可以找到的最佳解决方案(这不一定意味着它是最佳解决方案).

However, I am interested if it is possible to run Z3 for a limited amount of time and have it report the best solution it can find (which does not necessarily mean it is the optimal solution).

如果我在SMT公式上运行Z3并限制时间(通过参数-T)，如果它不能以最佳方式解决问题，它将仅报告超时".我读到默认的wmax解算器使用一个简单的过程来限制权重，并且很好奇是否可以从一个上限而不是一个下限来限制权重.

If I run Z3 on a SMT formula and restrict the time (via parameter -T), it will just report 'timeout' if it did not solve it optimally. I read that the default wmax solver uses a simple procedure to bounds weights and am curious to whether it is possible to bound the weights from an upper bound, rather than a lower bound.

关于， 埃米尔

推荐答案

超时选项-T导致进程终止，因此它不返回任何中间值.如果使用-t选项(软超时)，则该过程不会终止.相反，Z3会在检查取消的某个点停止搜索.然后产生到目前为止最好的答案.它对应于设置取消状态.我希望这对您有用.

The timeout option -T causes the process to terminate so it does not return any intermediate values. If you use -t option (soft timeout), then the process does not terminate. Instead Z3 will stop the search at some point where it checks for cancellation. It then produces the best answer so far. It corresponds to setting a cancellation state. I hope this will work for you.

这篇关于Z3限时优化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！