0

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!

Chemmyyu
  • 313
  • 1
  • 2
  • 7
  • 1
    Axel's answer gives a very nice example. However, it should be noted that while z3 can solve MILP, it'd be naive to expect it to beat custom solvers like Gurobi. Where z3 (and SMT solvers in general) shine is combination of theories, involving data-types, unbounded integers, reals, arrays, etc. Unless you have a need for this sort of combination of theories, you should stick to a dedicated MILP solver. (In particular, do not expect z3's optimizer to be speedy at all.) – alias Oct 31 '21 at 18:34

1 Answers1

2

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.

Look here and here for a discussion of alternatives.

Axel Kemper
  • 10,544
  • 2
  • 31
  • 54
  • 2
    Minor nitpick: The call to `o.maximize` at the bottom of the `while`-loop isn't necessary. It can be removed, saving the solver some headache as it'd have to at least recognize that it doesn't change the goal in any way. – alias Oct 31 '21 at 18:52