Search code examples
z3smt

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

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.

Solution

  • 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.