n×nn \times n Chess is EXPTIME-Complete

This is a question that I previously answered on quora. It seemed interesting enough to merit posting here as well.

Question

What is the proof for the claim that the n×nn \times n chess problem is not in PSPACE and harder than PSPACE-complete?

Answer

The paper by Fraenkel and Lichtenstein that proves this result (which was a real treat to glance over; more on that in a second) makes a few important assumptions. They define n×nn \times n chess to be chess on an n×nn \times n board (as you would expect), but they don’t make any assumptions about board configuration other than that both players have one king. (This means that black may have 45,000 light-square bishops and white may have 22 queens floating around, etc.) They also shrug off what a standard starting position might be on an n×nn \times n board and dispense with the move repetition draw rule. You might argue that this violates the spirit of the game. You would probably be right. So what is the problem that the authors are trying to solve?

The main problem is the following: given an arbitrary legal board configuration, how much time does it take to determine if there is a perfect strategy for one player (i.e. a move order in which winning is guaranteed)? This formulation gives us a more tangible place to begin.

In a paper on provably difficult combinatorial games, Stockmeyer and Chandra proved that a collection of very contrived-seeming two-person games is EXPTIME-complete. At the very highest level, the proof takes one of Stockmeyer and Chandra’s two person games and reduces it to a chess problem. If we were able to find a winning solution to the chess problem, we would then be able to solve the original EXPTIME-complete problem.

Now, the game that reduces to chess is a bit strange. As the authors did in the original paper, we will call it G3G_3. In G3G_3, there are two players W and B (in keeping with White and Black in chess) each of whom control a set of variables boolean denoted by XWX_W and XBX_B. There are also two Boolean formulas in 12DNF called W-Lose and B-Lose. The formulas are composed of some combination of the variables in XWX_W and XBX_B. The players take turns changing the value of one of the variables in the set they control in an attempt to make the other player’s losing formula true. If, say, W is able to make B-Lose true, B will have a chance to falsify it again. If B is unable to make a change that falsifies B-Lose, then W is the winner.

Here’s where things get interesting (and slightly ridiculous). Fraenkel and Lichtenstein managed to transform G3G_3 into a chess position in which the only legal moves correspond to making some Boolean variable in G3G_3 true or false. Only certain queens and rooks are able to move, and those pieces are trapped in a sea of deadlocked pawns and bishops. A small part of their creation looks like this:

../assets/images/white_boolean_controller.png

And this piece combines with other similar parts to create a representation of entire formulas like the one in this example:

../assets/images/global_w_lose.png

A winning strategy in this crazy chess game directly corresponds to a winning strategy for G3G_3, and the transformation can be done in polynomial time, so n×nn \times n chess is also EXPTIME-complete!

(This description obviously glosses over almost all of the finer details in the construction. Take a look at the original paper for those!)