[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...

[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