[mochomocha]

This is technically true but practically irrelevant. Case in point, I deployed at Netflix a real-time combinatorial solver specifically for CPU scheduling [1].

Most real-world combinatorial problems can be solved relatively well. This is why Gurobi is in business, Alpha Go exists, or why Amazon and United Airlines still manage to practically solve their resource allocation problems.

[1]: https://netflixtechblog.com/predictive-cpu-isolation-of-cont...

[skyde]

first time earing about Gurobi, is it some kind of SMT solver? I tried looking at their website but could only find high level marketing description.