Cairn

algorithms · game trees · O(tree size) worst case — touches ~31% of nodes on average in this page's own 20,000-tree sweep, never a fixed fraction like alpha-beta's b^(d/2)

↩ back to Game Trees

Proof-Number Search

Proof-Number Search answers a different question than every other entry in this category. Minimax, Monte Carlo Tree Search, and the rest all ask "what's the best move from here" and return one. Proof-Number Search asks "can this position's true value — win or lose for whoever's trying to prove it — be established outright, without visiting every leaf of the tree." It searches an AND/OR tree: an OR node is proven the moment any one of its children is proven (find one winning line and you're done), while an AND node is proven only once every child is proven (a forced sequence has to hold at every step). Instead of exploring depth-first like backtracking or minimax, it keeps two running counts at every node it has ever touched — a proof number (the fewest additional leaves that would need proving to prove this node) and a disproof number (the fewest that would need disproving to disprove it) — and always spends its next expansion on whichever untouched node currently looks likeliest to finish the job, re-deciding after every single expansion. Introduced by Victor Allis and colleagues in 1994, it's the search behind exhaustive endgame solvers and checkmate-puzzle engines, where a good-enough evaluation isn't the goal — a certain answer is.

Try it

A small, fixed AND/OR tree, 15 nodes deep across four levels. Every node's type (OR or AND) and every leaf's true value (Win or Loss, for the side trying to prove the root) is drawn up front for clarity — but the search itself only ever computes a proof/disproof number for a node once it actually visits it. Watch the table below the diagram: most rows stay blank the whole way through. Root is node 0, an OR node — press Step or Run to watch the search look for the fastest way to prove or disprove it.

Why it works

Every node keeps a proof number (pn) and a disproof number (dn). A proven leaf (a real win for the prover) gets pn=0, dn=∞ — nothing left to prove, and it can never be disproven. A disproven leaf gets the mirror image, pn=∞, dn=0. A node that exists but hasn't been looked at yet gets the optimistic default pn=1, dn=1 — as far as the search knows, one more expansion could resolve it either way. Two rules combine children's numbers into their parent's:

OR node:  pn = min(children's pn)   — proving the cheapest child proves the whole node
          dn = sum(children's dn)   — disproving it means disproving every child, one by one
AND node: pn = sum(children's pn)   — proving it means proving every child, one by one
          dn = min(children's dn)   — disproving the cheapest child disproves the whole node

The OR/AND rules are exact mirror images of each other, which is exactly why mixing them up (this page's first Pitfall below) is so easy to write and so wrong to run. To pick what to expand next, the search walks down from the root through already-touched nodes only, choosing the child with the smallest pn at an OR node and the smallest dn at an AND node, until it falls off the edge of what's been touched — that node, the most-proving node, is what gets expanded next. Expanding it means revealing its own children (or, if it's a leaf, learning its real value) and recomputing its own pn/dn from the rules above; then every ancestor back up to the root gets recomputed in turn, since a child that just changed can flip its parent's numbers too. The search stops the instant the root's own pn hits 0 (proven) or its dn hits 0 (disproven).

Run against this page's own demo tree, the whole thing resolves in 5 expansions: node 0 (root) first, revealing 1 and 2; then, because both look equally promising at their optimistic defaults, node 1; then node 2, for the same reason; then node 3, whose own two children (7, 8) turn out to both be real WIN leaves, proving node 3 outright after just one look; then node 4, whose child 9 is also a WIN leaf, proving node 4 the same way. The moment both of node 1's children (3 and 4) are proven, node 1 — an AND node — is proven too, which alone proves the root, an OR node, without the search ever touching nodes 5, 6, 11, 12, 13, or 14 at all. 11 of the tree's 15 nodes get touched; 4 never do — the entire right-hand subtree under node 2 turns out to be irrelevant to the proof, and best-first selection is exactly the mechanism that avoids wasting an expansion finding that out the hard way.

Reference implementation

function proofNumberSearch(root) {
  develop(root); // reveal the root's own children and compute its first pn/dn
  while (root.pn !== 0 && root.dn !== 0) {
    const mpn = mostProvingNode(root);
    develop(mpn);
    updateAncestors(mpn);
  }
  return root.pn === 0 ? 'proven' : 'disproven';
}

function develop(node) {
  if (node.terminal) {
    node.pn = node.isWin ? 0 : Infinity;
    node.dn = node.isWin ? Infinity : 0;
    return;
  }
  for (const child of node.children) { child.pn = 1; child.dn = 1; } // optimistic default
  updateNumbers(node);
}

function updateNumbers(node) {
  if (node.terminal) return;
  if (node.type === 'OR') {
    node.pn = Math.min(...node.children.map((c) => c.pn));
    node.dn = node.children.reduce((sum, c) => sum + c.dn, 0);
  } else { // AND
    node.pn = node.children.reduce((sum, c) => sum + c.pn, 0);
    node.dn = Math.min(...node.children.map((c) => c.dn));
  }
}

function mostProvingNode(root) {
  let node = root;
  while (node.developed && !node.terminal) {
    node = node.type === 'OR'
      ? node.children.reduce((a, b) => (b.pn < a.pn ? b : a))
      : node.children.reduce((a, b) => (b.dn < a.dn ? b : a));
  }
  return node;
}

function updateAncestors(node) {
  for (let cur = node.parent; cur; cur = cur.parent) updateNumbers(cur);
}

Pitfalls

Swap the OR and AND formulas and it isn't just wrong sometimes — it's wrong most of the time, and often doesn't even finish. The two rule sets above are structurally identical (one's min/sum pair mirrored into the other's sum/min), which makes swapping them a genuinely easy typo, not a contrived one. Run that swapped version against 20,000 randomly generated AND/OR trees, each checked against a brute-force full-tree evaluation: it returns a flatly wrong proven/disproven verdict on 4,198 of them (21.0%), and on 12,923 more (64.6%) it never terminates at all — the numbers can spiral without ever reaching a real 0, since the formulas no longer mean what the selection and stopping logic assume they mean. The smallest failing case is a 3-node tree: a root OR node with exactly two children, one a LOSS leaf and one a WIN leaf. The correct version proves the root instantly (pn=min(∞,0)=0) — one winning move is all an OR node ever needs. The swapped version computes pn=sum(∞,0)=∞ and dn=min(0,∞)=0 instead, and confidently reports the position as a forced loss, despite a winning move sitting right there as one of its exactly two choices.

Forget to walk back up to the root after expanding a node, and the search does all the right work — then never notices it's done. On this page's own demo tree, a version that develops each most-proving node correctly but skips updateAncestors entirely still expands nodes 0, 1, 2, 3, and 4 in the identical order the correct version does, computing every one of their pn/dn values correctly in isolation. But the root's own pn was only ever set once, right after its first expansion, and nothing ever tells it that node 1 (one of its two children) became proven three expansions later. The stopping check keeps reading the root's stale numbers forever, so the search takes a 6th step — walking down through already-resolved nodes since their pn/dn still correctly favor the proven side, straight into an already-terminal leaf — and tries to expand a leaf a second time, which is undefined for a node with no children to reveal. The proof was sitting complete in node 1's own numbers two full steps earlier; nothing ever carried that fact back up.

Complexity

Time: O(tree size) worst case — a pathological tree can still force every node to be touched before the root's numbers settle, the same worst case a plain full backward-induction sweep has. What makes proof-number search worth using is the practical case: because every expansion goes to whichever untouched node currently looks likeliest to finish the proof, it routinely stops well short of the full tree. This page's own 20,000-tree stress sweep (randomly shaped, depth ≤ 5, branching factor 2–3 at each internal node) touched an average of 30.9% of each tree's nodes before the root was proven or disproven, and matched a brute-force full-tree evaluation's verdict on all 20,000 — 0 mismatches. There's no fixed bound like alpha-beta's O(b^(d/2)) here, since how much gets skipped depends entirely on how early a short proof happens to sit. Space: O(nodes touched) — every node the search has ever expanded keeps its own pn/dn pair in memory for the rest of the search, unlike Minimax's O(d) recursion stack, which only ever holds one line of play at a time. That's proof-number search's real weakness against very large trees: it can run out of memory long before it runs out of time, which is exactly why practical implementations often cap how many nodes stay resident and fall back to re-deriving forgotten ones rather than storing the whole search graph forever.

This is the site's 11th Game Trees entry, and unlike every other one it never picks a move at all. Minimax, Monte Carlo Tree Search, and Expectimax all return "play here"; the three refinements (Principal Variation Search, MTD(f), and Killer Move Heuristic) all make that same return value cheaper to reach; Transposition Tables, Zobrist Hashing, and Quiescence Search all support that machinery without deciding anything themselves. Proof-Number Search instead answers a yes/no/unknown question about a whole subtree — can this be proven outright — which is why it shows up in exhaustive endgame databases and checkmate-puzzle solvers rather than in a clock-limited engine picking its next move. See Choosing a Game Tree Search Algorithm for how all eleven compare side by side.