What is the theory behind Z3 Optimize maximum and minimum functionality?

Question

I am writing to inquire the theory/algorithm behind the Z3 Optimize function, especially for its maximum and minimum function. This seems pretty magic to me. Is it somehow a binary search or so? How can it efficiently figure out the max/min value here..?

I tried to search for the source code of the related functions (e.g., the execute_min_max function), but without a deep understanding about the terms there, it does not make too much sense to me... Basically what does lex stand for here? It seems that somehow the solutions are maintained inside a stack.

Any suggestions or advices would be appreciated very much. Thanks.

Benzo

I don't know the whole answer, but I'd wager lex is short for lexicographic. – Docker

See publications on the topic like, 1. Nikolaj Bjorner and Anh-Dung Phan. νZ - Maximal Satisfaction with Z3. In Proc International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC). easychair.org/publications/?page=862275542 2. Nicolaj Bjorner, Anh-Dung Phan, and Lars Fleckenstein. Z3 - An Optimizing SMT Solver. In Proc. TACAS, volume 9035 of LNCS. Springer, 2015 -- And, if those are not enough, any other publication related to the topic of Optimization Modulo Theories. – Sos

@PatrickTrentin That should be an answer, not a comment! Spot on. – Topgallant

@LeventErkok I thank you for the suggestion, but the question seems to be a bit unclear and too broad for me to answer, as it inadvertently ask for details concerning many topics. I am also the least knowledgeable person on the internal details of z3 here, so I always try to keep my level of intrusion at minimum. If you think that the question is salvageable and can be given a proper answer, please don't be concerned about my half-assed suggestion in the comments feed, and proceed head on. I'll be happy to up-vote it, as always. (: – Sos

@patrick-trentin Your link to Bjorner and Phan didn't work for me, but this appears to be the paper: microsoft.com/en-us/research/wp-content/uploads/2016/02/…. Here's a link to the second paper as well: microsoft.com/en-us/research/wp-content/uploads/2016/02/…. The papers seem to overlap a bit, and if I had to choose one I'd choose the first one. – Docker

@MatthewWoodruff thank you very much, I'll update my database of bibliographic references accordingly. – Sos

Thank you so much for the kind notes. I appreciate it a lot. Would anyone post a answer here so I can credit accordingly? – Benzo

@PatrickTrentin Please turn your comment into an answer! (You misspelled Nikolaj's name in the second reference, just FYI.) – Topgallant

@LeventErkok thanks, fixed. – Sos

Answer 1

See publications on the topic like, e.g.

1. Nikolaj Bjorner and Anh-Dung Phan. νZ - Maximal Satisfaction with Z3. In Proc International Symposium on Symbolic Computation in Software Science, Gammart, Tunisia, December 2014. EasyChair Proceedings in Computing (EPiC). [PDF]

2. Nikolaj Bjorner, Anh-Dung Phan, and Lars Fleckenstein. Z3 - An Optimizing SMT Solver. In Proc. TACAS, volume 9035 of LNCS. Springer, 2015 -- And, if those are not enough, any other publication related to the topic of Optimization Modulo Theories. [Springer] [[PDF]

---

The z3 Optimization Modulo Theories (OMT) solver has various optimization procedures. Some of these techniques are more efficient than others, but can only deal with certain classes of objective functions (i.e. Pseudo-Boolean/MaxSMT objectives). In the case of Linear Arithmetic cost functions which cannot be reduced to Pseudo-Boolean/MaxSMT, the basic approach for the optimization search, adopted by most OMT solvers, is to run either in linear- or binary-search. For a comparison among the two approaches, see either

• Roberto Sebastiani and Silvia Tomasi Optimization in SMT with LA(Q) Cost Functions. In IJCAR, volume 7364 of LNAI, pages 484–498. Springer, July 2012. [PDF]

• Roberto Sebastiani and Silvia Tomasi. Optimization Modulo Theories with Linear Rational Costs. ACM Transactions on Computational Logics, 16(2), March 2015. [PDF]

I am not sure how to answer the question "How can it efficiently figure out the max/min value here..?", because first one should define what efficiency means in this context. As you can read from the previous two publications, binary-search is not always the best choice because search steps in optimization don't have all the same "cost".

The definition of lexicographic optimization is readily available all over the internet, this is the one I used very recently:

Definition 4.6.4. (Lexicographic OMT [BP14, BPF15, ST15b, ST15c]). Let <φ,O> be a multi-objective OMT problem, where φ is a ground SMT formula and O = { obj_1 , ..., obj_N } is a sorted list of N objective functions. We call Lexicographic OMT problem, the problem of finding the model M which satisfies φ and makes each obj_i minimum¹ in decreasing order of priority.

¹: in practice objectives need not to be all minimized, this is just for ease of definition

AFAIK, the lexicographic optimization procedure implemented in z3 is not extensively described in any publicly available paper. However, a trivial approach for lex is to run N single-objective (incremental) optimizations, each time fixing the optimum value obtained at the previous round.

---

If this is not enough to answer your questions, please take a look to any other publication related to the topic of Optimization Modulo Theories.

Sos

Great answer! Thanks for the extra references, in particular. – Topgallant

Fantastic! Thank you so much for this great answer! – Benzo