How can I specify to the Z3's optimizer to start the search from the lower bound of the objective function?

Kamugg 0
Viewed 18

I'm using Z3 to optimize a SMT problem. I have a variable "h" (obviously bounded by some constraints) that I want to minimize with the Z3 Optimize class. The point is that I know the lower bound of h but not its upper bound, so if I write something like

optimizer.add(h >= lower_bound)

what happens is that the solver spends a lot of time trying suboptimal values of h. If instead I write

optimizer.add(h == lower_bound)

the optimizer finds the solution for h fairly quickly if there is one. My problem is that clearly the optimal solution doesn't always have h == lower_bound, but it's usually close to it. It would be nice if there was a way to specify to the optimizer to start searching from the lower bound and then go up. A workaround that I found consists in using the Z3 Solver class instead of the Optimize one and iterating over all the possible values of h starting from the lower bound, so something like:

h = lower_bound
sat = 'unsat'
while sat != 'sat':
  solver = Solver()
  h_var = Int('h')
  solver.add(h_var == h)
  # all the other constraints here...
  sat = solver.check()
  h += 1

But it's not really elegant. Can some of you help me? Thank you very much.

z3py smt optimization python
1 Answers

If you know an upper bound as well, then you can do a binary search. That'd be logarithmically optimal in terms of the number of calls to check you have to make.

If you don't have an upper limit, then first find it by incrementing h not by 1, but by a larger amount to "jump" to an upper-bound. (For instance, increment by 1000 till you hit unsat.) Then do a binary search since you'll have upper-lower bounds at that time. Of course a good value for increment will depend on the exact problem you have.

I'm afraid these are your only options. The "official" way of doing this is to say opt.add(h >= lower_limit), which doesn't seem to be working for your problem. Perhaps the above trick can help.

Another thing to try is a different solver: OptiMathSAT has different algorithms and optimization techniques implemented. Perhaps it'll perform better: https://optimathsat.disi.unitn.it

useroBV30
Related