Closed tpaviot closed 3 years ago
I have the following idea: turn the multiobjective problem into a single one. If O_i and O_j are two objectives that have to be minimized, then minimize the objective O=W_iO_i+W_jO_j where W_i and W_j are integers that represent the objective weights. Solve this single objective using the IncrementalSolver, which has proved to have better performances than the standard optimization solver.
This issue is already solved right?
Yes, I think so. I close the issue. If ever there are new problems with multi-optimization performance, we will open a new ticket.
The built-in optimization solver for z3 appears to be weak regarding scalability. Works well for small problems. Larger problems take too much time to successfully report a solution.