0

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.

rusty_lurker
  • 17
  • 6

1 Answers1

0

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.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • Thank you for your response. -t option seems to work longer than specificied e.g. I specified -t:60, meaning 60 miliseconds, but it ran five minutes before I manually terminated it. But it does print a solution even when manually terminated, which is great! – rusty_lurker Nov 23 '15 at 11:42
  • One more small another issue: [here](http://rise4fun.com/z3opt/tutorialcontent/guide) I read that one can specify different optimization engines. However, when I write "(set-option :opt.wmaxsat_engine hsmax)", I get an error from Z3 "unknown parameter 'wmaxsat_engine' at module 'opt'". I used "opt.maxsat_engine" instead but the solution seems to disregard all constraints. Are other engines implemented currently? I uploaded the file [here](http://www.speedyshare.com/5RTHc/1dfb5107/smtInstance). Thank you in advance! – rusty_lurker Nov 23 '15 at 11:44
  • Soft timeouts could be ignored if there are long-running steps that don't check for cancellation. We rely on repros to determine where missing cancellations checks appear. There is no option wmaxsat_engine. the option you are thinking of is maxsat_engine. There are two main engines: wmax and maxres. The other (implemented) engines are inferior although they should be accessible. – Nikolaj Bjorner Nov 23 '15 at 20:11
  • Thank you for your very fast replies and help! – rusty_lurker Nov 24 '15 at 09:27