CODEWITHSUNDEEP
pythonz3
Chemmyyu
Chemmyyu

Reputation: 323

Can Z3 solve a MILP optimization problem? Can it output the top N best result?

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!

Upvotes: 0

Views: 906

Answers (1)

Axel Kemper
Axel Kemper

Reputation: 11322

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.

Upvotes: 5

Related Questions