"Left wins" has no short proof

Somebody says Left wins the 3×3 Domineering board moving first. What would settle it?

Not a move. A move can be answered, and the answer can be answered, and the claim is about all of that at once. What settles it is an object with a shape: Left’s move here, and then for each of Right’s replies, Left’s move there, and so on to the end.

The object, and why it is the shape it is #

A strategy branches where the loser chooses and does not branch where the winner does. That asymmetry is the whole definition and it is worth dwelling on, because it is what makes the object large.

At a node where the winner is to move, one option suffices: they only have to have a winning move, and naming a second would add nothing. At a node where the loser is to move, every option has to be there: a strategy that failed to say what to do against one reply would not be a proof of anything, since the opponent would simply play it.

The clearest way to see that the branching belongs to the loser is a board where the loser never gets a choice.

So the size of a strategy is governed by the loser’s branching factor, raised to the number of turns the loser gets. On the 3×3 board Right has two replies worth making and the game is over in four moves, and the whole object is six positions.

Change the game and the number moves violently.

Nim, where the proof is a hundred thousand times the answer #

Three heaps of 7, 11 and 13. The position graph has 480 positions — every triple of heap sizes no larger than the original — and a complete solution stores a verdict for each one.

Left’s winning strategy from that position has 56,167,022 nodes.

That is not a defect of the strategy. It is what a proof-by-cases costs when there are that many cases: Right may take any number from any heap, so at Right’s first turn there are thirty-one replies, at their second nearly as many, and the object answering all of them for eleven of Right’s turns grows accordingly.

The comparison is the point. Solving the game completely — a verdict for every position — costs 480 entries. Proving the verdict at one position, by exhibiting play, costs 56 million. The complete solution is smaller than the proof of one line of it by a factor of 117,000.

What a theorem does to that number #

There is of course a proof of the same claim that fits on a postcard.

The nim-sum of 7, 11 and 13 is 1, which is not zero, so the player to move wins. Anybody can check the arithmetic in a few seconds.

Written in binary, 7 is 0111, 11 is 1011 and 13 is 1101; add the columns without carrying and the answer is 0001. The nim-sum is not zero, so the player to move wins, and the winning move is whichever one makes it zero. Three exclusive-ors, no picture required, and it replaces fifty-six million nodes.

The postcard is not the strategy. It is an invariant, and the strategy follows from it by an argument that fits in three lines:

• the positions with nim-sum zero are exactly the ones the mover loses;
• from any position with nim-sum non-zero there is a move to nim-sum zero;
• from any position with nim-sum zero, every move leaves nim-sum non-zero;
• the empty position has nim-sum zero, and is lost by the mover.

Those four statements, together, generate the whole 56-million-node object without ever writing it down. That is what a theorem is, computationally: a compression of a strategy into something checkable in the length of the position rather than in the size of the play.

The two ways of knowing, side by side #

Set them against each other and the shape of the field appears.

The invariant is not always available. For Nim it is the nim-sum; for Wythoff’s game it is a pair of Beatty sequences and the golden ratio; for green Hackenbush it is fusion. For Domineering nobody has one, and for Domineering the only known proof of a claim about a board is the object drawn at the top of this page, at whatever size that board makes it.

That is the precise sense in which these games are hard, and it is much sharper than takes a long time. The difficulty is not that a search is slow. It is that nobody has found a short thing to hand over.

Where the size actually comes from #

It is worth pinning down which feature of a game makes its strategies large, because the answer is not the one intuition offers.

It is not depth on its own. Nim on 7, 11 and 13 runs to thirty-one moves, and a game of thirty-one moves in which the loser had one option throughout would have a strategy of thirty-one nodes.

It is not branching on its own either. A game where the winner has fifty options at every turn has a strategy no larger than one where they have two, because the strategy picks one and discards the rest.

The bottom of the range is a board on which the loser gets no turn at all.

Widen that board and the loser starts choosing.

What makes it large is the loser’s branching, compounded over the loser’s turns. Every option the loser has at every turn is a case the proof must answer, so the object grows like $b^{d}$ where $b$ is how many replies the loser has and $d$ is how many times they get to reply. The four Domineering boards above give Right two replies, one, none and four respectively, at a single turn each; Nim on 7, 11 and 13 gives Right thirty-one replies at the start and still a dozen halfway down, over eleven turns of theirs, and that is the whole of the difference between six nodes and fifty-six million.

It explains the priced table further up in the same way. Domineering on 4×4 has a strategy of 182 nodes because Right runs out of horizontal placements after four turns, and the boards drawn here are the same mechanism at sizes small enough to look at.

It also explains an inversion worth noticing: on the 4×4 Domineering board the strategy (182) is smaller than the table (5,700), and on the Nim position it is vastly larger. Which of the two objects is the cheap one is not a fact about the subject at all. It depends on the shape of the game.

Counting a strategy without building one #

Fifty-six million nodes is not a number arrived at by construction — building the object would take more memory than the machine has, and the first version of the code that produced this essay’s figures did exactly that and died.

The count comes from the same manoeuvre used everywhere else here. The size of the strategy from a position is one plus the size below it: one child at the winner’s nodes, all children at the loser’s. That recurrence depends only on the position and whose turn it is, so it is computed once per position-and-side pair — 960 of them for this Nim position — and the answer for the root falls out.

It is a small joke and a real technique: the object being called impractically large is measured exactly, in thirteen milliseconds, by the method whose absence made it large in the first place. Sharing subtrees is the whole difference between the graph and the tree, and it works just as well on a strategy as on a search.

The code refuses to draw what it happily counts. Anything over four hundred nodes is reported as a number and not built, and the figure generator refuses again at eight leaves, since a picture five thousand pixels wide is not a picture.

Why the class is what it is #

This is where the shape of a complexity class comes from, and the connection is worth making explicit.

A problem is in NP when a yes-answer has a short certificate — one that is polynomial in the input and checkable in polynomial time. Satisfiability qualifies: hand over the assignment. The natural game question does not obviously qualify, because the only certificate anybody knows is a strategy, and a strategy is exponential.

Games are known to be in PSPACE, which is a weaker and quite different guarantee: a decision procedure exists that uses only polynomial memory, by playing the game out and backtracking. That is a statement about running the search, not about being handed a proof. The reason space rather than time is the resource named is its own rung.

And PSPACE-complete problems are not known to be in NP. If a game question turned out to have short certificates, an entire class of problems would collapse into another one, and nobody expects that. So the honest statement is: no short proof is known, no theorem forbids one, and the whole weight of expectation is against.

Which collapse, exactly #

“An entire class of problems would collapse into another one” is the right instinct and it is worth spelling out, because the argument is three steps and each is short.

Suppose some PSPACE-complete game question had short certificates — that it were in NP. Every problem in PSPACE reduces to it in polynomial time, and NP is closed under those reductions, so every PSPACE problem would be in NP and $\mathrm{NP} = \mathrm{PSPACE}$. But PSPACE is closed under complement: a machine that decides a question in polynomial memory decides its negation in the same memory, by inverting the answer. So $\mathrm{co\text{-}NP} = \mathrm{co\text{-}PSPACE} = \mathrm{PSPACE} = \mathrm{NP}$, and the whole polynomial hierarchy above it falls in with them.

That is a very large consequence to follow from one game having a postcard proof, and it is the reason the expectation runs the way it does. Nobody expects $\mathrm{NP} = \mathrm{co\text{-}NP}$, and a short certificate for Domineering would deliver it.

The step that does the damage is the closure under complement, and games make it unusually visible. A finite game with no draws is determined: exactly one of Left wins and Right wins is true, and whichever it is, the witness is a strategy of the same shape. So the negative answer has a certificate of exactly the same kind as the positive one, which is not how NP problems usually behave — a satisfying assignment certifies satisfiability and nothing comparable certifies unsatisfiability.

The 3×3 board makes the symmetry concrete, because on it both players win moving first, and both claims cost the same to prove.

The symmetry is the whole difficulty, seen from the certificate side. For satisfiability there is an asymmetry to exploit and a class, NP, that captures one half of it. For a game there is none: the two answers cost the same to prove and neither is cheap, and any construction that made one of them cheap would make the other cheap too. That is what it means for the difficulty to live in the alternation rather than in the size — the previous rung’s finding, restated as a fact about proofs rather than about searches.

The claim is testable rather than merely stated, which is the one thing a certificate argument can offer a reader directly: be handed a board whose winner is named in advance, and try to be the exception.

It also says something about what a reader should expect from a new game. A game that turns out to be easy will be easy because somebody found an invariant, and an invariant certifies both answers at once — the nim-sum says who wins from every position, not merely from the winning ones. So the search for a short proof is not a search for a clever way to write down one strategy. It is a search for a property of positions that the moves respect, and if one exists it collapses both halves of the problem together, which is exactly why so few games have one.

The exception a reader will think of #

Surely, someone will say, one can just hand over the value — the number the recursion computes — and be done.

The value is small. A 4×4 Domineering board is worth a fourteen-node object; most values are far smaller than the searches that produce them. Handing it over would settle the outcome instantly, since the outcome follows from the value by comparing with zero.

The catch is that a value is not self-certifying. Handed the string this board is worth $\{0 \mid \ast\}$, the recipient has no way to check it short of computing it themselves — and computing it is the expensive thing. A certificate is only a certificate if verifying it is cheaper than doing the work, and a value fails that test exactly.

That is not a quirk of this site’s solver. Comparing two positions is itself decided by play — the relation between $G$ and $H$ is the outcome of $G - H$ — so there is no route to checking a claimed value that avoids solving something.

Compare it to the nim-sum, which does pass: the recipient computes three exclusive-ors of the input and matches the claim. The difference is not that one is a number and the other a tree. It is that one is a function of the position that can be recomputed cheaply, and the other is the output of the search being replaced.

Even checking that two claimed values are equal is a search of the same kind: the question of whether $G$ equals $H$ is the question of who wins $G - H$, and answering it means solving a position built out of both. So a value handed over as a claim cannot be verified by inspection, and cannot be verified by comparison with another claim either.

A strategy that is not a tree at all #

There is a third form the object can take, and it is the one every playable figure on this site actually ships.

A table — position to move — is a strategy written as a lookup rather than as a tree. It is no larger than the position graph, since each position appears once, and it answers every reply the loser can make because every reachable position is in it. The Nim position that needs 56 million nodes as a tree needs 480 rows as a table.

That is not a contradiction; it is the same collapse as before. A tree stores one entry per route and a table one per position, so the ratio between them is the ratio this site has been counting all along.

The catch is that a table is not a proof in the sense this essay started with. Handed 480 rows, a sceptic must check each one — that the move named leaves a position from which every reply is again in the table with a good answer — and that check is a pass over the whole table, which is a pass over the whole solved game. The tree is checkable by playing; the table is checkable by re-solving; the invariant is checkable by arithmetic. Only the last is cheaper than the work it replaces.

The sizes are worth a Clobber example, because the three objects come apart there too. A $2 \times 3$ Clobber board of alternating stones is worth zero, so the player to move loses; the table certifying that is 117 positions, and the winner’s strategy from the opening is 35. Thirty-five is small enough to hand over and check by playing, on a board with six stones on it — and the table beside it is three times larger and cheaper to check only in the sense that a sceptic has to re-solve the game either way.

What the picture cannot show #

The strategy drawn at the top is complete and it is complete for a nine-square board. Three limits follow.

The figure refuses to draw the interesting cases. A 3×4 strategy has eleven leaves and would run over a thousand pixels wide; a 4×4 strategy has forty-seven and would run to five thousand. The generator throws rather than producing them, which is the honest behaviour and also means every strategy a reader sees here is a small one. The numbers in the table above are the way to see what happens at size.

A minimal strategy may be smaller than the one drawn. At each of the winner’s turns this construction takes the first winning move it finds, not the one leading to the smallest remaining strategy. Choosing better would shrink the object somewhat — and not by an order of magnitude, since the loser’s branching is what dominates, and no choice by the winner reduces it.

Nothing here is a lower bound. That no short certificate is known for Domineering is a statement about what people have found. A clever invariant for it could be discovered tomorrow, and the whole of this essay’s arithmetic about that game would become a historical curiosity — exactly as it did for Nim, which looks trivial only because Bouton found the invariant in 1901.

The 3×4 board is where that limit begins to bite. Right wins it whoever moves first, and Right’s strategy from the opening is thirty-six positions with eleven leaves — small enough to hold in a file and already too wide to draw on a page. A playable figure of that board answers a reader’s moves from a table of all 550 of its positions, which is a different object again: it is not the proof, it is the thing the proof is about.

Who framed it this way #

The certificate view of NP is Cook and Levin’s, around 1971, and the reason it reshaped the subject is that it moved attention from how long does solving take to what would have to be handed over. The two are related and they are not the same question, and the second turns out to be the one that classifies problems tidily.

For games the corresponding observation is older than the vocabulary. Bouton’s 1901 paper on Nim does not compute anything: it exhibits a property of positions, proves the three closure claims, and stops. That is the earliest example in this subject of a strategy compressed to an invariant, and every closed form since has the same shape — the simplicity rule, Sprague–Grundy, fusion, the Beatty sequences of Wythoff’s game.

Which suggests the right way to read a hardness result about a game. It is not a claim that the game is deep or subtle. It is a claim that no such invariant exists to be found — or, in the cases that are only conjectured, that nobody has managed it yet, and that a great deal else would follow if they did.

The next rung takes the other resource. If the difficulty is not that a proof is long but that a search is large, what exactly runs out first — and why is the class named after memory rather than time?