Multi-objective Mixed Integer Programming and Z3

Vilfredo Federico Damaso Pareto (1848-1923) [link]

The tool \(\nu Z\) [1,2] is an optimization extension to the SMT solver Z3 [3]. It can actually generating Pareto optimal solutions for MIP problems, using an algorithm based on [6]. In [4,5] a small example model is presented:

\[\bbox[lightcyan,10px,border:3px solid darkblue]{ \begin{align}\max\>&x_1 – 2x_2\\ \max\>&-x_1+3x_2\\ &x_1 \le 2x_2\\ &x_1,x_2 \in \{0,1,2\}\end{align}}\]

There are 5 different Pareto optimal solutions. Let’s see how we can implement this in Z3 using Python:

This looks promising. I have some large instances lying around. I am curious how this solver will behave on those.

A real surprise

We have to be very careful when using floating point coefficients. If we divide the first objective by 2, we should get the same Pareto front. However what we see is:

What happened here? No, error messages, no warnings, but obviously the results are wrong. We can see what happened by printing:

Our 0.5 has become 0! (I am yelling now: keep your hands off my data!).

After some experimentation, I came up with the following workaround:

Now we get:

The results for z1 indicate the solver actually reports rational values. Indeed the printed model has:

(A bit funny. I would expect 0.5 or (/1 2) but not this mixture.)

See [7] for some background on why this is happening. (I think I would never do this rounding without raising some kind of exception: it is just too dangerous. A little bit ironic that Z3 is used a lot to do program correctness verification.).

References

1. Nikolaj Bjørner, Anh-Dung Phan, and Lars Fleckenstein, \(\nu Z\) - An Optimizing SMT Solver, https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf
2. Nikolaj Bjørner and Anh-Dung Phan, \(\nu Z\) - Maximal Satisfaction with Z3, in Proceedings of International Symposium on Symbolic Computation in Software Science (SCSS), 2014, https://easychair.org/publications/open/xbn
3. The Z3 Theorem Prover, https://github.com/Z3Prover/z3 
4. Generating all non-dominated solutions in a multi-objective integer programming model, http://yetanothermathprogrammingconsultant.blogspot.com/2010/02/generating-all-non-dominated-solutions.html
5. Sylva, Crema: A method for finding the set of non-dominated vectors for multiple objective integer linear programs, EJOR 158 (2004), 46-55.
6. D. Rayside, H.-C. Estler, and D. Jackson, The Guided Improvement Algorithm for Exact, General-Purpose, Many-Objective Combinatorial Optimization, Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009, https://dspace.mit.edu/bitstream/handle/1721.1/46322/MIT-CSAIL-TR-2009-033.pdf
7. https://stackoverflow.com/questions/46721639/z3-and-interpretation-of-floating-point-coefficients