CODEWITHSUNDEEP
optimizationz3
Ian
Ian

Reputation: 31

How to improve the optimization speed of z3?

I use Z3 to solve linear optimization, but with the increase of variables and constraints, the solution time is unbearable. In the future, the number of variables is about 35940 and constraints are probably more than a hundred thousand。 Is there a way to improve speed?

from z3 import *
opt = Optimize()
cost=Int('cost')

[varibles and constraints]

set_option(max_args=1000000)
set_option(max_lines=1000000)
h=opt.minimize(cost)
print(opt.check())
m=opt.model()
print (m)
print(opt.lower(h))
doc=open('result.txt','w')
print(opt.model(),file=doc)

Upvotes: 3

Views: 406

Answers (1)

alias
alias

Reputation: 30418

As posed, this question is unanswerable. You said nothing about the nature of your constraints (are they linear, simple equalities, 1-0's only?), nor anything about the application domain itself. Keep in mind that z3's optimizer is a very general "hammer." Yes, it'll optimize your linear constraints, but where it shines is in theory combination, not in its speed. If your domain has a custom optimization algorithm, you should, by all means, use that. With 40K variables and 100K constraints, unless they are all boolean and rather trivial, I wouldn't expect z3 to perform all that well. But then again, it all depends on the nature of these constraints.

Having said all that, reading through the z3 optimization paper is your best bet to understand how it works internally; it can help at least decide whether you should invest in a custom algorithm. See here: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf

Upvotes: 3

Related Questions