Capture-Quiet Decomposition: A Verification Theorem for Chess Endgame Tablebases

TL;DR

The paper introduces the Capture-Quiet Decomposition theorem, a structural approach for verifying chess endgame tablebases by decomposing positions into terminal, capture, or quiet categories, ensuring correctness through external verification.

Contribution

It provides a novel verification method that decomposes endgame positions and validates WDL labelings using smaller verified sub-models, improving verification reliability.

Findings

Validated on 517 endgames with 42 million positions

Decomposed verifier matched full retrograde baseline in all cases

Breaks circularity in self-consistent labeling verification

Abstract

We present the Capture-Quiet Decomposition (CQD), a structural theorem for verifying Win-Draw-Loss (WDL) labelings of chess endgame tablebases. The theorem decomposes every legal position into exactly one of three categories -- terminal, capture, or quiet -- and shows that a WDL labeling is correct if and only if: (1) terminal positions are labeled correctly, (2) capture positions are consistent with verified sub-models of smaller piece count, and (3) quiet positions satisfy retrograde consistency within the same endgame. The key insight is that capture positions anchor the labeling to externally verified sub-models, breaking the circularity that allows trivial fixpoints (such as the all-draw labeling) to satisfy self-consistency alone. We validate CQD exhaustively on all 35 three- and four-piece endgames (42 million positions), all 110 five-piece endgames, and all 372 six-piece endgames -- 517 endgames in total -- with the decomposed verifier producing identical violation counts to a full retrograde baseline in every case.