1

I'm trying to minimize a variable, but z3 takes to long in order to give me a solution.

And I would like to know if it's possible to get a solution when timeout gets triggered.

If yes how can i do that?

Thx in advance!

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Andre Oliveira
  • 45
  • 6

1 Answers1

2

If by "solution" you mean the latest approximation of the optimal value, then you may be able to retrieve it, provided that the optimization algorithm being used finds any intermediate solution along the way. (Some optimization algorithms --like, e.g., maxres-- don't find any intermediate solution).

Example:

import z3

o = z3.Optimize()
o.add(...very hard problem...)
cf = z3.Int('cf')
o.add(cf = ...)
obj = o.minimize(cf)
o.set(timeout=...)
res = o.check()
print(res)
print(obj.upper())

Even when res = unknown because of a timeout, the objective instance contains the latest approximation of the optimum value found by z3 before the timeout.

Unfortunately, I am not sure whether it is also possible to retrieve the corresponding sub-optimal model with o.model() (or any other method).

For OptiMathSAT, I show how to retrieve the latest approximation of the optimum value and the corresponding model in the unit-test timeout.py.

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
  • Thx for the help! But I'm getting minus infinite (-1*oo) Do you know why? – Andre Oliveira Mar 27 '19 at 15:10
  • Im trying to minimize – Andre Oliveira Mar 27 '19 at 15:56
  • Another question: Can I instead of using timeout to exit, can i use an if condition? If yes, how can i do that? – Andre Oliveira Mar 27 '19 at 15:58
  • I guess it's the lower bound -- If minimeze gets lower than a certain limit exit from solver – Andre Oliveira Mar 27 '19 at 16:24
  • @AndreOliveira In minimization the `lower` is updated upon *unsatisfiable binary-search steps* and the `upper` is updated upon *satisfiable linear-/binary-search steps*, so you ought to check the value of `obj.upper()`. I didn't find anything in `z3`'s API to do the other thing you have asked about. It would be pretty trivial to do it with `OptiMathSAT`, using either the option `opt.abort_interval` or the option `opt.abort_tolerance`, or by writing a custom `msat_termination_test` callback function. – Patrick Trentin Mar 27 '19 at 16:41