CODEWITHSUNDEEP
optimizationz3smttheorem-provingsatisfiability
Halaby
Halaby

Reputation: 49

How does "minimize" work in Z3

I'm using the minimize function in Z3 a lot and I'm worrying about some scalability issues (when the number of variables I'm minimizing grows). What is the underlying algorithm of "minimize" and is there a general way to speed things up?

Upvotes: -2

Views: 766

Answers (1)

alias
alias

Reputation: 30525

See this paper for details on the optimization algorithms used in Z3. Regarding your question about "general way to speed things up:" Impossible to tell without seeing exactly what you're trying to do and how you are encoding it. Posting a concrete example where things don't "scale" might be helpful.

Upvotes: 1

Related Questions