Pareto fronts in Z3: a large data set

In [1] a small multi-objective MIP is solved with Z3. Here we try a larger problem, an engineering design problem. It has three objectives and 2029 non-dominated solutions. The solution in the F space (the objectives) looks like:

To make life easier for Z3, I converted the objectives to integer values. The good news is that Z3 finds the same number of solutions. The bad news: for this problem it is not very fast:

We see it is getting slower and slower:

The first 500 solutions are found in a rate of about a second per solution. Later on this becomes 10 seconds per solution.

Brute force

A brute force method for this problem is:

1. Generate all feasible integer solutions for this problem. I used Cplex for this, using the solution pool technology. I get about 4.8 million solutions.
2. Filter out all dominated solutions. There are 2029 remaining non-dominated solutions.

This method takes about 20 minutes (i.e. 1200 seconds).

References

1. http://yetanothermathprogrammingconsultant.blogspot.com/2017/10/multi-objective-mixed-integer.html