Z3 Time Restricted Optimization

问题:

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.

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).

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.

Regards, Emir

回答1:

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.