Hard, proved

The exact evaluator runs out of room after a few dozen moves, and every essay on this site says so where it matters. That is an observation about a program. This is the theorem that says no program does better.

The theorem needs a game simple enough that nothing about it can be blamed for the difficulty — no partizan asymmetry, no board, no pieces — and there is one.

The game #

Six vertices, eight arrows, a token. There is nothing to it, and that is the point: any difficulty in deciding who wins cannot be attributed to a complicated rule, a large branching factor or an unbounded board. The board is a graph and the rule is one sentence.

The game is finite for an easy reason — every move uses up a vertex, and there are finitely many — so the recursion is grounded and the outcome is well defined, which is not something a game with loops in it can say. The number of positions is at most the number of (vertex, visited-set) pairs, which is $n \cdot 2^n$, and the whole game can be unrolled in space proportional to the depth.

That last fact places the problem in PSPACE: decidable by a machine using polynomial space, however much time it takes. The interesting claim is that it is as hard as anything in that class.

Formulas as games #

A quantified boolean formula is a logical sentence with its variables bound in order, like

$$\exists x_1 \, \forall x_2 \, \exists x_3 \;\; (x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_2 \vee x_3).$$

Deciding whether such a sentence is true is the standard hardest problem in PSPACE, and there is an obvious reason: the alternating quantifiers are a two-player game. The existential player picks values for the odd variables wanting the formula true; the universal player picks the even ones wanting it false.

If that game can be drawn as a geography position — if any formula can be turned into a graph on which the token game has the same winner — then geography is at least as hard as the formula, and the theorem follows.

How the graph works #

There are two stages and the graph enforces both.

The assignment. Each variable gets a diamond: a top, two middle vertices labelled with the variable’s two literals, and a bottom. The player to move at the top chooses a middle vertex; the other player is then forced to the bottom; the first is forced on to the next diamond. Three moves per diamond, so the choosing alternates exactly as the quantifiers do.

The convention that makes it work is the one that looks backwards. Passing through the vertex labelled $\ell$ makes $\ell$ false, because passing through it uses it up. A player who wants $x_1$ to be true walks through the vertex labelled $\neg x_1$.

The challenge. After the last diamond the token reaches a single vertex from which every clause is reachable. The player to move there is the universal one, and it names a clause it claims is unsatisfied. The existential player must then move from that clause vertex to one of its literals — and every literal vertex has already been visited if the assignment made that literal false, so the move exists exactly when the clause contains a true literal.

If the existential player can move, they do, and from a literal vertex the only edge leads back to a bottom already used, so the universal player is stuck and loses. If the existential player cannot move, they lose immediately.

So the existential player wins the game exactly when every clause the universal player might name has a true literal — exactly when the formula is satisfied by the assignment the diamonds produced. And the diamonds produce whatever assignment optimal play produces, which is the quantified formula’s own semantics.

Following one game through #

The graph is easier to trust once a token has been walked over it, so here is one line of play on the two-clause formula the figure draws.

The formula is $\exists x_1 \forall x_2 \exists x_3$ over the clauses $(x_1 \vee \neg x_2 \vee x_3)$ and $(\neg x_1 \vee x_2 \vee x_3)$. Note that $x_3$ appears positively in both, so setting it true satisfies everything and the formula is true. The existential player should therefore win.

Moves one to three. The token is at the top of the first diamond and the existential player moves. Wanting $x_1$ true is optional here — $x_3$ will carry both clauses — so either middle vertex is fine. Say it passes through the vertex labelled $\neg x_1$, making $\neg x_1$ false and $x_1$ true. The universal player is forced to the bottom; the existential player is forced on to the second diamond.

Moves four to six. The universal player chooses at the second diamond and will pick whichever middle vertex hurts most. It passes through the one labelled $x_2$, making $x_2$ false. Forced moves take the token to the third diamond.

Moves seven to nine. The existential player chooses again, passes through the vertex labelled $\neg x_3$ — making $\neg x_3$ false, so $x_3$ true — and the token arrives at the challenge vertex.

The challenge. The universal player names a clause. Whichever it names, the vertex labelled $x_3$ is unvisited, so the existential player moves there. From $x_3$ the only edge goes to a bottom already used. The universal player cannot move and loses.

The formula is true and the existential player won, which is what the reduction promised. A construction that only ever reports true would have promised nothing, so the same drawing is worth having for a formula that is false.

Take the four clauses $(x_1 \vee x_2 \vee x_3)$, $(x_1 \vee x_2 \vee \neg x_3)$, $(\neg x_1 \vee x_2 \vee x_3)$ and $(\neg x_1 \vee x_2 \vee \neg x_3)$ under the same quantifier prefix. The universal player sets $x_2$ false, and what is left of the four clauses is $(x_1 \vee x_3)$, $(x_1 \vee \neg x_3)$, $(\neg x_1 \vee x_3)$ and $(\neg x_1 \vee \neg x_3)$ — which every one of the four assignments of $x_1$ and $x_3$ falsifies. The formula is false, and the graph has to say so.

Walking it out reaches the challenge vertex with a clause every one of whose literal vertices has been used, and the existential player stuck. That is the negative answer arriving by the same route as the positive one, which is the property a reduction has to have and the one a single worked example cannot demonstrate.

That is the whole proof, and the useful thing about walking it is noticing how much of it is forced. Six of the nine assignment moves have exactly one option, and the choices happen at four vertices out of fifteen — the three diamond tops and the challenge. The reduction spends most of its structure making sure the free choices fall to the right players in the right order.

What the solver computed, and how #

A drawing of a reduction is a picture of an argument. The argument is only worth anything if the two things it claims are the same really are the same, and that is checkable.

The check is exhaustive over a stated family. Over three variables there are eight possible three-literal clauses, so $255$ non-empty formulas, and every one is done both ways.

The formula route evaluates the quantifiers directly: recurse on the variables, taking a disjunction at existential ones and a conjunction at universal ones, and test the clauses at the leaves. It knows nothing about graphs.

The game route builds the graph from the clauses, then solves the token game by the ordinary recursion over (vertex, visited-set) pairs. It knows nothing about logic — it has a set of arrows and a rule about not revisiting.

All $255$ agree, and a single disagreement would stop the figure drawing.

The site’s gate runs the same check and then does something more useful: it breaks the reduction on purpose and requires the disagreement to appear. Deleting the challenge vertex, so that the existential player picks which clause to defend rather than the universal player picking which to attack, is the endgame backwards — and the check catches it on a large fraction of the family.

One sabotage that is not caught is worth recording, because mistaking it for a passing test would be an error. Inverting every literal in every clause leaves the answers unchanged, because it renames every variable to its own negation and the game is symmetric under that. A gate that used it as its rejection test would be reporting that it had verified something it had not.

Where the theorem stops #

This is the most misread result in the subject, so the boundaries are worth drawing carefully.

It is about a family, not a position. “Generalized Geography is PSPACE-complete” means: no algorithm decides every geography position in polynomial time, unless a great many other things collapse. It says nothing about any particular graph. The six-vertex position at the top of this page was decided in microseconds.

Hardness is a lower bound on the worst case. A problem can be hard and have easy instances — most instances easy, even. Real positions from a real game are not adversarially constructed, and the hardness result gives no reason to expect them to be difficult.

It does not say a game is uninteresting. The reduction constructs graphs that no player would produce. That those graphs are hard tells a player nothing about the graphs they will meet — and a game with no hardness result at all can still be unsolved, for entirely different reasons.

“Generalized” is load-bearing. The theorem is about geography on arbitrary graphs of arbitrary size. Every fixed finite game — chess on eight by eight, Go on nineteen by nineteen — has a constant-size answer and is not hard in this sense at all. Hardness results about board games are always about the generalised family.

And the arrows are load-bearing too. The theorem is about directed geography, and taking the arrows off the same edges gives a game whose rules differ by one word — a token, a move to any neighbour not yet used, and a player with no such neighbour loses.

That is the sharpest statement available here of what an arrow costs. The undirected game is decided by a matching — Fraenkel, Scheinerman and Ullman’s theorem of 1993 — in time polynomial in the graph, and the winning strategy is the matching itself: move along a matched edge and the reply is forced back onto an alternating path the matching’s maximality closes off. Put the arrows back and no such criterion is known or expected, because the family is complete for the class.

The two are also worth comparing vertex by vertex rather than in the aggregate. Geography is impartial — the token is nobody’s, and both players have exactly the same moves from any position — so every starting vertex carries a Grundy value rather than merely an outcome. Directed, the six vertices of the first figure have Grundy values 1, 0, 0, 2, 1, 1, so two of them are second-player wins; undirected, every one of the six is a first-player win. One word of the rule changed the outcome at two vertices and removed the search entirely.

What the reduction does that a proof sketch does not #

The usual presentation of this result is three paragraphs of prose and a diagram nobody has checked. Building it has two payoffs beyond confidence.

The first is that the parity has to be right. Three moves per diamond, the challenge falling to the universal player, the literal move being the last one — every one of those is a place where an off-by-one makes the reduction reduce the wrong formula, and the exhaustive check finds each of them immediately. A prose proof can carry such an error for a long time.

The second is that the shape of the argument becomes visible. Looking at the drawn graph, the diamonds are plainly a sequence of binary choices with alternating owners, and the clause section is plainly a challenge and a reply. A reader who sees that has understood the reduction in a way that a reader who has followed the prose has not, because the prose has to describe a picture and the picture is the thing.

What the drawing cannot show #

The reduction figure is a graph with labelled vertices and arrows, and four things about it are invisible.

It cannot show the parity. Whose turn it is at each vertex is the entire content of the construction, and a static graph has no turn in it. The colouring asserts which player chooses where; the assertion is justified by counting three moves per diamond, and the count is in the prose rather than in the picture. A graph drawn with the colours swapped would look equally plausible and would be a reduction of the wrong formula.

It cannot show the visited set. A geography position is a vertex and a set of vertices already used, so the drawing shows a board rather than a position. Everything interesting happens in the set, and the set is not drawable without drawing the whole game.

It cannot show the theorem. Nothing here proves that quantified boolean formulas are hard; that is imported. The drawing establishes a connection between two problems, and the difficulty flows along it from a source somewhere else entirely.

And it cannot show why the game ends. Every move here uses a vertex up, so no line of play returns to where it was and the recursion has somewhere to bottom out — a property the drawing quietly depends on and does not display, since a graph with a cycle in it looks exactly like a graph without one. A game that can return to a position it has already been in has no outcome to compute at all, let alone a hard one, and the difficulty this page is about is a difficulty that only arises once the answer exists.

Completeness is two arguments and only one of them is the reduction #

A completeness result is often quoted as though it were the reduction alone, and the reduction is half of it. Both halves are needed and they say different things.

The reduction is a lower bound. It shows that anything in the class can be turned into a game question in polynomial time, so the game question is at least as hard as everything in the class. On its own that leaves the game possibly harder — it could sit far above the class and the reduction would look identical.

Membership is the upper bound, and for games it is the easy direction: play the position out depth-first, holding one line and the moves already tried at each level, and back up. The memory is the depth of a line, which is bounded by the board because every move consumes something that cannot come back. The time is every route and is exponential, which the class permits.

Only the pair pins the problem to the class. Hardness alone is a statement about how much difficulty the game contains; membership alone is a statement about how little; and completeness is the two meeting, which is what makes the classification informative rather than a bound in one direction.

That is worth carrying because the two halves are proved by completely different means and fail for completely different reasons. A reduction is a construction — wires, gates, crossovers built out of board positions — and checking it is checking that the pieces behave. Membership is an algorithm, and it is the algorithm nobody would ever run: the one that puts these games in PSPACE is precisely the one that re-derives everything instead of remembering it.

The generalisation #

Geography is the entry point rather than the destination. The same technique — draw the formula as the game — has been used to establish hardness for a long list of games people actually play, and the pattern is always the same: find a gadget that implements a binary choice, another that implements a clause test, and wire them together with the parity correct.

Generalised Go, generalised chess, generalised checkers, Hex, Amazons, Othello: all hard, all by reductions of this shape, and in several cases the gadgets are considerably more ingenious than these diamonds because the game’s rules make binary choices awkward to build.

There is a second direction that matters more to this site. The hardness results are about deciding a single position, and the theory here is about evaluating sums. Deciding who wins a sum of trivially easy components is itself hard — a result about the sum operation rather than about any game in it — and that is the sharpest form of the observation that additivity of values does not make the game easy.

Who found it, and when #

Thomas Schaefer proved Generalized Geography PSPACE-complete in 1978, in a paper that established hardness for a whole catalogue of games at once and introduced the technique this essay draws.

The quantified boolean formula problem had been shown PSPACE-complete by Stockmeyer and Meyer a few years earlier, and geography’s proof is a reduction from it — which is the ordinary shape of such results and is why every one of them is ultimately a statement about drawing a formula.

The subsequent history is a catalogue. Fraenkel and Lichtenstein established generalised chess in 1981; Robson did Go in 1983 and checkers in 1984; and the list has been extended steadily since, with each new game requiring its own gadgets and its own parity argument.

What has not happened is any narrowing of the gap between the theorem and practice. Programs play these games well, and the hardness results are entirely compatible with that, because the positions programs meet are not the positions the reductions construct.

Where the ladder goes next #

The complexity anchor has two rungs to here: how hard the games are, and the classification with its reduction.

Nim is easy is the contrast the classification needs — a family in the same subject settled by three exclusive-ors at any size — and how a position is written down then shows that even that claim depends on the encoding: three heaps of a thousand are thirty digits or three thousand counters, and the same three operations read as linear against one and as better than linear against the other.

“Left wins” has no short proof asks the question from the certificate side and measures the object: 480 table entries for a complete solution of a Nim position against 56,167,022 nodes for a winning strategy from one of its openings. It also supplies the argument this page’s classification only gestures at — if a game question had short certificates then NP would equal PSPACE, and PSPACE’s closure under complement would give $\mathrm{NP} = \mathrm{co\text{-}NP}$.

Space is the resource names the quantity the class is about, out of three a 4×4 Domineering board supplies: 6,257,129 routes, 5,700 positions, and a deepest line of eight moves. And what solved means collects the four senses of the word — an argument that names no move, a formula that names one from anywhere, a strategy for a single opening, and a database — which are four different answers to is this game solved and disagree because they are four different questions.