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 phases 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. Running the same walk on a false formula finds the challenge vertex offering a clause every one of whose literal vertices has been used, and the existential player stuck.

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.

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

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.

The ladder from here #

This anchor began with how hard it is — a measurement of where the evaluator stops. This rung is the theorem behind the wall.

Later rungs: the space bound in detail, and why the game is in PSPACE at all. Undirected geography, which is in polynomial time by a matching argument and is the closest thing the subject has to an easy hardness boundary. The gadgets used for a real board game, where the binary choice has to be built out of stones or pieces. The complexity of sums of easy games, which is where hardness meets the theory this site is about. And the honest question of what a hardness result should change about how anybody plays, which is very little and is worth saying out loud.

The thing established here is a drawing that was checked. The reduction is the argument, the argument is a picture, and every formula in a stated family was played both ways before the picture was allowed on the page.