A different question at every depth
Assumes: A move whose every reply is struck · A shortlist with nothing at the top
A move whose every reply is struck turned the Sylver Coinage pairing test into a proof. The test strikes a move when the position it reaches has gaps pairing off around the largest one, because such a position is a win for the player who moves next. A survivor is a move the test does not strike. A position is proved won within one move if some survivor leaves the opponent only struck replies, within three if some survivor leaves every surviving reply a position proved within one, and so on. Deepened one odd depth at a time, that proves every irreducible position to sixteen gaps by thirteen moves — and costs more, on every one of the 583, than a search that simply skips struck moves and plays to the end.
Its diagnosis was specific: the proof is rebuilt from nothing at each depth, so a search that kept the positions it had proved or refuted, and never asked about them again, would cost less. The open question was whether it would cost less than the finishing search, and whether that might happen on positions larger than sixteen gaps, where the finishing search is dearer.
It costs less than the forgetful proof. It does not cost less than the finishing search, on any position to twenty gaps, and the reason is not forgetting.
Four proofs and one search
The census is every irreducible position — gaps pairing off around the largest — with up to twenty gaps: 1,766 positions, 583 of them to sixteen gaps as before and 1,183 more from seventeen to twenty. Every search is charged in closures, one per move examined, the unit the earlier essay used, so every number here is comparable with its.
The finishing search is the baseline: memoised on positions, stopping at the first winning move, skipping every move the test strikes. It asks one question of each position — is it won? — and stores one bit.
The fresh proof is the earlier essay’s: deepen over survivors at depths 1, 3, 5 and so on, with a new table at each depth.
The kept proof keeps one table across all depths. For each of the mover’s positions it records the shallowest depth at which the position was proved won, with the move, and the deepest at which it was refuted — no win within that many moves. At the next depth a position already proved at a shallower depth is proved, and one already refuted at a deeper or equal depth is refuted, without looking.
The two directions of reuse are the whole of what a kept table can offer, and both come from one fact: the answers are monotone in the depth. A position won within five moves is won within seven, because a proof that finishes early is still a proof. A position with no win within seven has no win within five, because a win within five would be one within seven. So a stored proof answers every deeper question and a stored refutation every shallower one. What neither answers is the question in between — a position refuted at five and asked about at seven — and that is the question a deepening search asks most.
The two-sided kept proof does the same for the opponent’s positions as well. The earlier proof handled the opponent’s turn inline: for each candidate move it walked every surviving reply and asked about the position after it. That walk is not remembered, and a position of the opponent’s reached from two different candidates is walked twice. Kept as a table entry of its own — every surviving reply leads to a position won within so many moves — it is walked once per depth at most.
The told proof is the one no deepening scheme can beat: it is handed the right depth in advance, searches only at that depth, and memoises both players’ positions there. It is the price of the proof itself, with the cost of finding the depth taken away.
The counts are the result. The fresh proof is cheaper than the finishing search on none of the 1,766 positions, the kept proof on none, and the two-sided kept proof on none. Their median costs are 13.6, 8.4 and 5.4 times the finishing search’s. The told proof, the floor for any deepening, is cheaper on seven positions and costs 2.5 times the finishing search at the median.
A saving that loses ground
Keeping the table works in the sense the earlier essay predicted.
The kept proof is cheaper than the fresh one on 1,610 of the 1,766 positions, and its advantage grows with the positions: it costs 0.99 times the fresh proof at ten gaps, 0.73 at sixteen and 0.59 at twenty. Positions refuted at depth seven are not re-refuted at depth nine; positions proved at depth five are not re-proved at seven. Keeping the opponent’s positions as well cuts another quarter or so.
And the kept proof falls further behind the finishing search as the positions grow, from 3.8 times at ten gaps to 8.2 at sixteen and 9.7 at twenty. The fresh proof’s cost against the finishing search grows faster than the saving: from 3.9 times at ten gaps to 18.7 at twenty. Keeping the table removes a fixed share of a price that is rising, and the finishing search’s own cost rises more slowly still. So the particular hope the earlier essay left — that larger positions, where the finishing search is dearer, would tilt the comparison — is answered the other way. The finishing search is dearer at twenty gaps, with a median of 967 closures against 269 at sixteen — 3.6 times as dear for four more gaps — and the kept proof, whose ratio to it rises from 8.2 to 9.7 over the same step, grows by more than four times. Each added gap multiplies both costs, and the proof’s multiplier is the larger one.
The proofs larger positions need
The other half of that hope was that larger positions might often be proved shallowly, where a proof is cheap.
It is the reverse. At up to twelve gaps 36.7 per cent of positions are proved within three moves; at thirteen to sixteen, 3.7 per cent; at nineteen and twenty, 0.7 per cent — five positions of 732. The median depth of a proof climbs from five to nine to thirteen, and the deepest from nine to seventeen. The shallow proofs are a feature of small positions, where a survivor often leaves the opponent nothing the test has not struck. In larger positions there are more survivors, more surviving replies to each, and a proof has to go deep, which is where it is dearest.
Where the price comes from
The told proof isolates what is left when deepening is free, and it is still two and a half times the finishing search. The obvious suspects are ruled out by one measurement.
The told proof visits the same positions as the finishing search — the median ratio of the two sets’ sizes is exactly one. It is not wandering into parts of the game the finishing search avoids. What it does differently is ask about each of those positions several times: a median of 2.9 evaluations per position over the whole census, rising from 1.25 at ten gaps to 3.3 at twenty.
The reason is in what the question is. The finishing search asks of a position is it won?, stores the answer and never asks again, whatever route it arrives by. A proof bounded by depth asks is it won within d moves?, and a position reached by one route with seven moves left and by another with eleven is two different questions with two different answers. A position that is won in nine moves is refuted at seven and proved at eleven. Keeping the table lets the proof reuse an answer to the same question and a stronger answer to a weaker one — proved within five is proved within seven — but it cannot turn not within seven into anything useful at nine. The finishing search’s answer is the limit of all of those questions, and it is the only one that is asked once.
One position from the census shows it happening. The root has fifteen gaps — 1 to 8, 10, 11, 13, 14, 16, 19 and 28 — and the proof told its depth settles it at seven moves. On the way it reaches the position whose gaps are 1, 2, 3, 4, 7 and 8 twice: once with three moves left, where naming 8 proves it won, and once with one move left, where nothing does and it is refuted. Both answers are right. They are answers to different questions, and the finishing search, which reaches the same position, asks it once — won — and is done with it.
That is the same accounting the tree and the graph makes about routes: a position reached eleven ways is one position, and a search that treats it as eleven pays eleven times. A depth-bounded proof is a search that treats one position as several, by depth rather than by route.
Why deepening pays elsewhere and not here
A reader who has written a chess program will find this backwards, because in chess iterative deepening with a transposition table is the standard way to search and it pays. The difference is instructive, and it is a difference in what a shallow search is for.
In chess a search cut at a fixed depth ends in a guess — an evaluation of material and position — and the guesses from depth six are used to order the moves at depth seven. A good order makes the deeper search cheaper by far more than the shallower searches cost, and deepening is really a way of buying an order. There is also a clock: a program that must move in thirty seconds wants a move at every depth it completes, and deepening is the only way to have one.
Here neither applies. The shallow searches end in no guess: a position not proved within five moves is simply not proved, and nothing about it suggests which survivor to try first at seven. The kept table does carry one ordering hint — a move that proved a position at a shallower depth is tried first at the next — but a position proved at a shallow depth is already finished, so the hint only ever applies where it is not needed. And there is no clock, because the order the moves are tried in and where a search may stop are both about games small enough to finish. Deepening is a technique for games too large to finish, and the price measured here is what it costs on a game that is not.
Seven positions where a proof would pay
The exceptions are a family rather than a scatter. Six of the seven have gaps 1 to 5, then every odd number up to some point, then one larger gap; the seventh is a twenty-gap position of a different shape. In every one the move that wins is 7 and the proof finds it at depth five (depth nine for the odd one out). The finishing search, trying moves in increasing order, has to dispose of 2, 3, 4 and 5 first, and on these positions the depth bound makes those refutations shorter than the finishing search’s own. Why these positions and no others is not measured here, and seven of 1,766 is not a regime a solver could aim for — least of all a deepening one, which pays for every shallower depth before it reaches the one it was told.
What this settles about proofs and searches
Two claims from earlier essays meet here and turn out to be one.
A move whose every reply is struck found that a proof over survivors never beat the pruned search, and blamed rebuilding. Search on in pairs of moves found, in Domineering, that a certificate by deepening got cheaper only by turning into the search that finishes. The kept proof removes the rebuilding and the gap remains; the told proof removes the deepening and the gap remains. What is left is the depth in the question, and the only way to remove that is to stop bounding the depth — at which point the proof is the finishing search.
That makes the finishing search, on a game small enough to finish, not merely cheaper than any proof tried but the limit every proof approaches as it is improved. A strategy is not a certificate draws the distinction between knowing a move and being able to show it; the measurement here says that on these positions, showing it within a stated number of moves costs about three times knowing it, and that the factor grows with the position.
The rules and the counting
Sylver Coinage under the convention the game that is a number system sets out: players name positive integers in turn, a number that is a sum of numbers already named may not be named, and naming 1 loses, so 1 is left out of every move list. A position is a numerical semigroup and its gaps are the numbers still available. The census is every semigroup with up to twenty gaps whose gaps pair off around the largest, taken from an enumeration whose counts by genus are checked against the published ones — 8,045, 13,467, 22,464 and 37,396 semigroups at seventeen to twenty gaps. Every search tries moves in increasing order and counts one closure per move examined; every proved move is checked against the full search’s verdict.
What 1,766 positions cannot show
Twenty gaps is still small. The trend in every column is monotone over the range, and nothing here says it continues; a proof whose cost grew more slowly than the finishing search’s past some size would reverse the comparison, and the range does not reach it.
The move order is fixed. Every search tries moves smallest first. The seven exceptions suggest the order matters to the comparison, and a proof with a better order — or a finishing search with a worse one — could move the counts.
The told proof is a floor for these proofs, not for every proof. It memoises each position once per depth at which it is reached, which is the best a proof keyed on depth can do. A proof that stored, for each position, the exact number of moves in which it is won — its remoteness — would answer every depth at once, and it is not priced here, because computing a remoteness is itself a search that finishes: it is the finishing search with one more number kept.
And only one kind of proof is priced: deepening over survivors, with the opponent’s struck replies treated as settled. A proof that bounded something other than depth — the number of positions examined, say — asks a different question and is not measured.
Still open: whether a better order changes the verdict
Every search here tries the smallest move first, and the seven positions where a told proof wins are positions where the winning move comes fifth in that order. The measurement that would say whether order is the whole story is the same census with the finishing search and the proofs both trying survivors in the order a shortlist with nothing at the top scored — by the quantity that put a winning move first most often — and in its reverse. If the told proof’s seven grows to many under some order, a proof with the right order is competitive and the question becomes whether a deepening scheme can find that order cheaply. If the seven stays seven, the depth in the question is the whole price and the finishing search is where this line of improvement ends.
Part 7 of 7
One argument about Sylver. The parts either side of it:
The objects named here
The third axis, after the field and the series: the games, values and theorems themselves, and every essay that touches each one.
CertificateExhaustive searchMemoisationNumerical semigroupProofSearch costSylver CoinageTransposition table
- The pairing removes moves it cannot name certificate, exhaustive search, numerical semigroup, search cost, sylver coinage
- A check bit halves the average and not the key exhaustive search, memoisation, search cost, transposition table
- A key shorter than the position exhaustive search, memoisation, search cost, transposition table
- Proving a loss means answering everything certificate, exhaustive search, proof, search cost
- Two ways to end with no bound exhaustive search, numerical semigroup, proof, sylver coinage
- A count that forgets memoisation, search cost, transposition table