I am working on a MILP problem, and I need to output the top N best result. Someone suggest to use Z3 solver, as I never use this solver before, and I checked some docs, seems it is not a common optimization solver like Gurobi/cbc. Can someone help on this? If possible, can provide any examples in python? Thanks a lot!
You can solve MILP problems using Z3:
from z3 import *
# https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-optimization
o = Optimize()
x, y, z, gain = Ints('x y z gain')
o.add(2*x + 3*y + z == 100)
o.add(x + 2*y + 4*z == 25)
o.add(gain == 4*x + 7*y + 1*z)
o.maximize(gain)
noOfSolutions = 0
while (noOfSolutions < 10) and (o.check() == sat):
noOfSolutions = noOfSolutions + 1
model = o.model()
print(model)
# go for the next solution with reduced gain
o.add(gain < model.eval(gain))
Note that this code won't find solutions with the same non-decreasing value for gain.
To achieve that, a more involved constraint has to be added to prevent the previous solution to be chosen again.