← Back to context

Comment by LPisGood

5 days ago

My first thought is that there is surely an Integer Linear Programming approach that can solve this within a few seconds using some very advanced solver like Gurobi.

These solvers can very often find the globally optimal solution - and prove that this solution is optimal - much faster than exhaustive search.

Of course they do use a smart exhaustive search by applying branch-and-bound as described in this article, but advanced solvers use, among other things, branch-and-cut where cutting planes in the solution space are generated, as well as a variety of other approaches.

One interesting thing however is that GPUs are still not particularly applicable for solvings Mixed Integer Linear Programs to sufficient accuracy. There are things like PDLP that can use GPUs to solve these problems, but they are restricted to something like 1e-4 accuracy whereas the state of the art is more like 1e-9.

I actually did try ILP, see https://stackoverflow.com/questions/79422270/why-is-my-z3-an...

I tried Z3 and OR Tools. I didn't try Gurobi. But this was enough to make me think ILP was a dead end. (There were a lot of dead ends in this project.)

I don't know much about integer programming, though, and I'd love to be proven wrong.

  • I saw that! In my experience, problems that seem completely intractable using open source tools often get solved in seconds using state of the art commercial approaches.