In  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.
A brute force method for this problem is:
- 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.
- Filter out all dominated solutions. There are 2029 remaining non-dominated solutions.
This method takes about 20 minutes (i.e. 1200 seconds).