How do you set a timeout for the z3 optimizer such that it will give you the best known solution when it runs out of time?
from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())
Follow-up question, can you set z3 to randomized hill climbing or does it always perform a complete search?
Long answer short, you can't. That's simply not how the optimizer works. That is, it doesn't find a solution and then try to improve it. If you interrupt it or set a time-out, when the timer expires it may not even have a satisfying solution, let alone an "improved" one by any means. You should look at the optimization paper for details: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf
It is true, however, that z3 does keep track of bounds of variables, for numerical quantities. You might be able to extract these, though in general, you'll have no means of knowing what values out of those intervals you'd need to pick to get a satisfying solution for the overall problem. See this answer for a discussion: Is it possible to get a legit range info when using a SMT constraint with Z3
This sort of "hill-climbing" questions come up often in this forum. And the answer is simply that's not how z3's optimizer works. Some prior questions in this manner:
There are few other questions along these lines in stack-overflow. Search for "optimize" and "timeout".
That's the theory side of it. In practice, I believe the best approach to deal with a problem of this sort is not to use the optimizer at all. Instead do the following:
unsat. Quit.Still have time?
5a. Compute the "cost" of this model. i.e., the metric you are trying to minimize or maximize. If you store the cost as a variable in your model, you can simply query its value from the model.
5b. Assert a new constraint saying the cost should be lower than the cost of the current model. (Or higher if you are maximizing.) Depending on how fancy you want to get, you might want to "double" the cost function, or implement some sort of binary-search to converge on a value faster. But all that is really dependent on the exact details of the problem.
5c. Ask for a new model. If unsat, return the last model you got as "optimal." Otherwise, repeat from step 3.
I believe this is the most practical approach for time-constraint optimization in z3. It gives you the full control on how many times to iterate, and guide the search in any way you want. (For instance, you can query for various variables at each model, and direct the search by saying "find me a bigger x, or a smaller y, etc., instead of looking at just one metric.) Hope that makes sense.
Note that an SMT solver can work like you're describing, i.e., give you an optimal-so-far solution when the time-out goes off. It's just that z3's optimizer does not work that way. For z3, I found the iterative loop described as above to be the most practical solution to this sort of timeout based optimization.
You can also look at OptiMathSAT (http://optimathsat.disi.unitn.it/) which might offer better facilities in this regard. @Patrick Trentin, who reads this forum often, is an expert on that and he might opine separately regarding its usage.