Proof-Number Search

Purpose: A best-first search for proving or disproving a binary goal in a game tree (“can White force a win?”), rather than computing a numeric value. It expands the node that is cheapest to resolve, which makes it exceptionally good at finding narrow forced wins.

The Two Numbers

Every node carries:

• pn (proof number) — the minimum number of leaf nodes that must be proven TRUE to prove this node;
• dn (disproof number) — the minimum number of leaves that must be proven FALSE to disprove it.

Terminal nodes:

State	pn	dn
proven TRUE	0	∞
proven FALSE	∞	0
unknown leaf	1	1

Internal nodes:

• OR node (the player to move needs one winning child):
  $\mathrm{pn}={\min }_c\mathrm{pn}(c),\mathrm{dn}={\sum }_c\mathrm{dn}(c).$
• AND node (every child must be winning):
  $\mathrm{pn}={\sum }_c\mathrm{pn}(c),\mathrm{dn}={\min }_c\mathrm{dn}(c).$

Algorithm

while root.pn != 0 and root.dn != 0 and budget remains:
    n = root
    while n is not a leaf:                       # select the most-proving node
        if n is OR:  n = child minimising pn
        else:        n = child minimising dn
    expand n, evaluate its children
    update pn/dn back up to the root

The selected leaf is the most-proving node: proving it advances the proof of the root by the largest amount, and disproving it likewise advances the disproof. That single leaf serves both goals at once, which is the elegant part.

Why it beats alpha-beta on this problem

Alpha-beta searches to a uniform depth. Proof-number search follows the shape of the tree: it dives deep into narrow forced sequences and ignores wide branches where nothing is forced. For endgame and puzzle solving — where the answer is a long forced line — this is enormously better.

Famous result: checkers was solved (Schaeffer et al., 2007) using proof-number search variants as a major component.

Variants

Variant	Improvement
PN²	a second-level PN search at each leaf; drastically less memory
df-pn (depth-first PN)	reformulates as depth-first with thresholds; linear memory, the standard modern version
PDS	proof-number and disproof-number iterative deepening
Weak PNS	initialise unknown leaves with heuristic pn/dn instead of 1/1
Lambda search	combines PN search with threat-space search

Plain PNS stores the whole tree in memory, which is its main weakness; df-pn is what you use in practice.

Where it shows up

• Endgame solvers for checkers, Go life-and-death, shogi tsume problems, Hex, connect-6
• Puzzle solving where the question is “is this position winnable?”
• Contest use — rare, but the idea is transferable: when searching for a witness, expand the node that is cheapest to resolve rather than searching uniformly. That is a useful instinct for constructive search problems generally.

Variants / Use Cases

• Alpha-Beta and Negascout — for value search rather than proof search
• MCTS — also best-first, but statistical rather than exact
• Combinatorial Games — the theory of win/loss positions
• Branch and Bound — the same “expand the most promising node” philosophy in optimisation