linear programming - Solving MIP efficiently problems with z3

Question

I have a reasonably simple MILP (mixed integer linear program): https://0bin.net/paste/B1IE5l8l#2YLLrptC-l1ml+vesA59tH3167IOCAkJoIUQWbrj/mN

which I can solve with cbc optimally on my low-end computer in about 6.75 seconds.

I have tried to convert it to a format that z3 can take, making a few simplifications along the way and have this: https://0bin.net/paste/M5dDXNl2#-A3hnStDDZABP69+yBsCdEz818pif15r88SxD8qRwjX

but after half an hour I had to kill it without a solution.

Is there some trick I'm missing, or is z3 bad at solving these sort of MILPs?

question from:https://stackoverflow.com/questions/66056792/solving-mip-efficiently-problems-with-z3

Answer 1

Waitting for answers