A proof inside a budget

Where a search may stop found a way for a search that stops short to know it is right. Deepen one move at a time, guess at the leaves that any player with a move wins, and stop when two consecutive depths agree: an even depth can only overstate the player to move and an odd depth can only understate, so agreement pins the truth. Search on in pairs of moves combined that certificate with a window that declines to guess where the two players’ counts of placements are close, found that the window must search on two moves at a time to keep the proof, and priced the result. On four small Domineering boards the certificate was never cheaper than the memoised search that simply finishes, however the window was chosen.

That comparison has a weakness, and the essay named it. A certificate is priced against a search that finishes, which is only possible on a board small enough to finish. The certificate’s purpose is the other kind of board, where the finishing search cannot be afforded and the choice is not between a proof and an answer but between a proof and nothing. There the right question is not which is cheaper on average, but how often a proof arrives within a budget at all, and whether the window makes proofs arrive where plain deepening never does.

A board too large to finish cannot be used to check the answers, so the test is simulated on one that can. Every method is run to completion and its full cost counted; a method has a proved verdict within a budget when its cost is at most that budget. A program on a larger board, with a cap on the positions it may expand, would get exactly those verdicts and no others.

The positions a larger board is made of #

A random position of 4 × 5 Domineering is near its end: drawn from all 48,670, the mean longest line left is about three moves. On those positions no method has anything to save, and a budget comparison measures nothing but overhead. A larger board would spend its search on openings and early middlegames — positions with many moves still to play — so the sample here is drawn from the 2,364 positions whose longest line left is six moves or more, a thousand of them with a fixed seed.

Four methods are compared. The search that finishes is the memoised who-wins search, trying first the move that leaves the opponent fewest replies, with a table keyed by position. Deepening to agreement is the certificate: iterations of depth nought, one, two and so on, each with its own table keyed by position and depth left, guessing any mover wins at the cut, stopping when two consecutive depths agree or when an iteration consulted no guess. And two windowed certificates, which decline to guess where the counts are close and search on two moves there: one with the one-sided window that suits the bracket’s guess — decline where the mover is level or behind — and one with the symmetric window of plus or minus one placement.

Every verdict every method returns is right. That is not a finding; a certificate that could be wrong would not be a certificate, and the two-move windows were chosen because they keep the proof. What differs is only when each verdict arrives.

Budget by budget #

With sixteen positions to spend, the finishing search proves 227 of the thousand; the one-sided certificate proves 135; deepening to agreement and the symmetric window prove none. At 64, finishing has 840, the one-sided certificate 717, the symmetric window 207 and plain deepening 45. At 128, finishing has proved 991 — nearly all — while deepening to agreement has proved fewer than half. Everything is proved by 4,096, and the finishing search had everything but one by 512.

The last column is the one the question is about: positions a certificate proves within a budget where the finishing search, given the same budget, has proved nothing. It is three, once — the one-sided certificate at a budget of 32 — and one at 64, and nought at every other budget for every certificate. On the deep positions of this board, a program choosing between a certificate and a finishing search under a cap on positions expanded would have done better to finish at every cap tried, save three positions in a thousand at one of them.

Every kind of position, and the openings #

Two other samples bracket the deep one.

Drawn from every position of the board, the sample is dominated by endings, and on an ending the finishing search is a handful of positions: two at the tenth percentile, four at the median. A certificate needs at least two iterations, each of which pays for the positions it touches again, so it cannot be cheaper than something that costs four. Not one of the thousand positions is proved by a certificate inside a budget the finishing search misses.

At the other end are the openings: the 33 positions of the board with eight or nine moves still to play, the empty board among them. These are the positions a larger board would be made of at the start, where the search’s whole budget goes. The finishing search proves seventeen of them within 128 positions and all by 1,024. Deepening to agreement proves none by 256 and needs 4,096 for all of them. The one-sided window stays close to finishing — ten by 128, twenty-one by 256 — and never passes it. At no budget does any certificate prove an opening the finishing search has not.

Three boards, one ordering #

The same comparison on 4 × 4 and 3 × 6, again on the positions with six or more moves left, gives the same order on every board: finishing, then the one-sided window, then deepening to agreement a long way behind. On 4 × 4 there are only 218 such positions, all of them sampled, and by a budget of 64 the finishing search has proved 212, the one-sided window 159 and deepening to agreement 57. On 3 × 6 there are 717, and the three counts are 655, 564 and 195. The proportions are close to 4 × 5’s 840, 717 and 45 — the certificate by agreement is the method that varies most from board to board, and it is last on all three. The extra positions a certificate proves are a handful on each board, at one or two budgets, and never a trend. Nothing here grows with the board. The margin by which finishing leads narrows as budgets rise, but only because both are running out of positions to prove.

Why finishing wins where it cannot finish #

The reason is the one the tree and the graph supplies for Domineering’s small boards generally, and it survives the change of question. The finishing search keys its table by position alone, so a position reached along a second line is answered at once. Each deepening iteration keys by position and depth left, starts with an empty table, and cannot use anything the previous iteration learned. A certificate needs at least two iterations that guess somewhere, and on a deep position those iterations revisit the same shallow part of the tree at every depth.

A budget does not change that arithmetic, because the budget is spent in the same order. A strategy is not a certificate found the same ordering in Nim at a far larger scale — a proof that one position is won dwarfed the table that answers every position — and the reason there was the same as here: a table that remembers is worth more than any argument that has to be rebuilt. The finishing search’s cost on a position is the size of the part of the graph it must visit to prove the answer, visited once. The certificate’s cost is the same part of the graph, cut at depth d, summed over every d up to the depth where two iterations agree. Whatever a budget allows the finishing search to see, it allows the certificate to see less of, and see it more than once.

The windows narrow the gap in a telling way. The one-sided window declines to guess where the mover is level or behind, and on those positions it searches on — which is to say, it finishes them. The more positions a window declines to guess on, the more the certificate becomes the finishing search with iterations bolted on. Search on in pairs of moves found the same on average, that the certificate gets cheaper only by turning into the search that finishes; the budget curves say it position by position and budget by budget.

Where a certificate is cheaper at all #

The one place a certificate can win is a position where agreement arrives well before the longest line and the finishing search, for all its memory, has to walk that line out.

Deepening to agreement is cheaper than finishing on none of the thousand deep positions. The symmetric window is cheaper on none. The one-sided window is cheaper on twenty, with a mean longest line of 6.3 moves, and saves a mean of about an eighth of the finishing search’s cost there. Twenty positions in a thousand, and an eighth on each: that is the entire case for a certificate on this board, and it is not a case for using one where finishing is out of reach, because nothing picks out the twenty in advance.

What a proof costs, across the distribution #

Read as a distribution, the cost to a proof is 36 positions for the median finishing search and 135 for the median certificate by agreement, nearly four times as much. The one-sided window’s median is 38, a hair above finishing, and above the median it falls further behind: 73 against 54 at three quarters, 184 against 74 at nine tenths. The worst deep position costs 513 positions to finish and 1,590 to 2,785 to certify. The tail is where a larger board lives — the positions whose search is expensive are exactly the ones a budget runs out on — and in the tail every certificate is dearer, not cheaper.

What deepening is actually for #

The result is a clean negative about proofs, and it should not be read as a negative about iterative deepening, because proofs were never what deepening was for.

A program under a time limit does not need a proof. It needs a move when the clock runs out, and what makes iterative deepening the standard design is that it always has one: after every completed iteration it holds a verdict for the root and a best move, and each iteration’s verdict is at least as informed as the last. The finishing search has nothing at all until it finishes. Cut it off at a budget and it returns no verdict and no move; cut deepening off and it returns the verdict of the deepest completed iteration. A verdict that changes with the depth measured how good those interim verdicts are on this very board: guessing that the player with more placements wins, a search cut at depth nought is right on 72.5 per cent of positions and on almost all of them by depth seven.

So there are two budget questions, and they have opposite answers. Asked how many proved verdicts arrive within the budget, the finishing search wins at every budget on every board here. Asked how good is the answer held when the budget runs out, the finishing search holds nothing on every position it has not finished and deepening holds a guess on all of them. The certificate was an attempt to make the second kind of answer into the first — to let the interim guesses announce, occasionally, that they are no longer guesses. The budget curves say how often that announcement comes before the finishing search would have had the answer anyway: almost never.

That changes what the certificate is. It is not a way to search a large board; it is a free label on the few positions where the guesses happen to have settled. Its cost is paid in the iterations deepening was going to run regardless, if deepening was the design. For a program that deepens for the sake of its interim guesses, the certificate costs nothing extra and occasionally says this one is proved. For a program that wants proofs, it is the wrong search.

Where the budget goes #

The budget curves have one more feature worth reading, which is how the four methods spend a budget as it grows. The finishing search’s curve rises steeply and saturates: its cost is concentrated, and most deep positions cost between twelve and seventy-four positions to finish. The certificates’ curves rise late and slowly, because each iteration’s cost is spent before any agreement can be seen, and agreement needs the second of two agreeing iterations to complete. A certificate proves nothing until it has paid for at least two iterations that each touch every line to the cut, and on a deep position those two iterations are already most of the finishing search’s cost.

The one-sided window changes the shape more than the height. Where the mover is level or behind it searches on, and on this board that means it searches such positions to the end; it behaves like the finishing search on exactly the positions where a guess would be weakest. Its curve therefore hugs the finishing search’s low down and falls away above the median, where the iterations it still has to run begin to cost more than they save. Space is the resource is the other half of the ledger, and it runs the other way: the finishing search keeps a table of everything it has visited, while each deepening iteration’s table is thrown away. On a board where memory rather than positions expanded is the budget, that is the ground a certificate would have to fight on.

What the simulation assumes #

The budget is a cap on positions expanded, counted the same way for every method: a position is expanded when a search first asks about it with a given key, and a table hit costs nothing. Deepening’s iterations each start with a fresh table, as in the essays before; a program that carried its table across iterations, keyed by depth, would pay less, and nothing here prices that variant. Both searches try moves in the fewest-replies order, the order the order a solver tries the moves in found cheapest. Memory is not capped — the finishing search’s table grows with what it visits, and on a board where memory rather than time is the binding limit, the comparison could come out differently.

What four small boards cannot say about a large one #

The simulation is of a large board by small ones, and the step from one to the other is an assumption. The deep positions of 4 × 5 have longest lines of six to nine moves; a position on a large board may have forty. The finishing search’s advantage rests on its table reusing positions reached by different routes, and on a larger board the fraction of the graph a budget reaches is smaller, which could make the reuse matter less. Nothing measured here says whether it does. What is measured is that on every board small enough to check — and on the deepest positions of the largest of them — the reuse matters more than anything the certificate saves.

Still open: a certificate that keeps its table #

Every certificate here starts each iteration from nothing, because that is how iterative deepening is usually run and how the bracket was proved. The obvious repair is a certificate that keeps what earlier iterations proved: a position whose verdict one iteration established exactly, because its lines ended before the cut, need never be searched again. A different question at every depth tried exactly that repair on Sylver Coinage and found it cheaper than a fresh proof and never cheaper than the pruned finishing search. Whether the same holds on Domineering — whether a certificate that remembers its exact verdicts closes the gap to the finishing search, or passes it on the openings where budgets run out — is the measurement this leaves, and it is the last obvious place for the certificate to earn its keep.