Thursday, October 19, 2017

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