[dbatten]

Genuinely interested in being educated here: If Gurobi's integer programming solver didn't find a solution better than 218, is that a guarantee that there exists no solution better than 218? Is it equivalent to a mathematical proof?

(Let's assume, for the sake of argument, that there's no bugs in Gurobi's solver and no bugs in the author's implementation of the problem for Gurobi to solve.)

I guess I'm basically asking whether it's possible that Gurobi got trapped in a local maximum, or whether this can be considered a definitive universal solution.

[Tobs40]

Author here!

Yes, if Gurobi and my code run as intended and I did not mess up any thinking while simplifying my chess model, then what I did is proof that the maximum number of legal moves available in a chess position reachable by a sequence of legal moves from the starting position is 218 (upper and lower bound). Gurobi proved the entire search space as "at most as good" using bounds, basically.

[salt4034]

In addition to the value of the best integer solution found so far, Gurobi also provides a bound on the value of the best possible solution, computed using the linear relaxation of the problem, cutting planes and other techniques. So, assuming there are no bugs in the solver, this is truly the optimal solution.

[dbatten]

Unless I missed something, though, the highest bound the author reported for the relaxation was 271 2/3 moves, which is obviously significantly higher than 218...

[salt4034]

I think that was an intermediate model. The author updated it, then Gurobi solved the new model to optimality (i.e., the bound became equal to the value of the best solution found).

> With this improved model, I tried again and after ~23 000 seconds, Gurobi solved it to optimality!

[dbatten]

> Gurobi solved the new model to optimality (i.e., the bound became equal to the value of the best solution found).

Ah, I was not aware that that's what this language indicated. Thanks for helping me understand more!

I've used Gurobi (and other solvers) in the past, but always in situations where we just needed to find a solution that was way better than what we were going to find with, say, a heuristic... I've never needed to find a provably optimal solution...

[hyperpape]

The article was interesting, but this bit felt a bit like "and then a miracle occurred".

[chipsrafferty]

The fractional stuff was poorly explained, I didn't understand it at all.

[gregdeon]

I'm not sure about Gurobi or how the author used it in this case. But in general, yes: these combinatorial solvers construct proof trees showing that, no matter how you assign the variables, you can't find a better solution. In simpler cases you can literally inspect the proof tree and check how it's reached a contradiction. I imagine the proof tree from this article would be an obscenely large object, but in principle you could inspect it here too.

[nhumrich]

In theory, it's not proof. In practice, it is.

[sigbottle]

Well, if the solver isn't wrong and there were no bugs in impl, yes, the approach is rigorous. Allow strictly more "powerful" configurations yet still prove that the maximum is X, then achieve X through a construction, is standard math