St John's bridge

It is possible to completely solve some endgames, so that for every position you can tell whether White wins, loses or draws with best play for both sides. In all of the following positions White can force checkmate, but only after the longest possible line of defence.

Checkmating a Bare King

  • King and 2 Rooks versus King: longest win is mate in 7.
  • King and Queen versus King: longest win is mate in 10.
  • King and Rook versus King: longest win is mate in 16.
  • King and 2 Bishops versus King: longest win is mate in 19.
  • King, Bishop and Knight versus King: longest win is mate in 33.

Basic Endgames

  • King and Queen versus King and Rook: longest win is mate in 35.
  • King and Queen versus King and Bishop: longest win is mate in 17.
  • King and Queen versus King and Knight: longest win is mate in 21.
  • King and Rook versus King and Knight: longest win is mate in 40.
  • King and Rook versus King and Bishop: longest win is mate in 29.

For more longest wins see the complete list of four piece pawnless endgames.

Correctness

This guest lecture explains how formal verification is used to prove that the solutions of these endgames are correct with respect to the laws of chess. The following research paper surveys the (few) errors that have crept into endgame solution implementations over the years, and defines the class of errors that can be prevented by using formal verification:

  • CANONICAL CITATION: Joe Hurd and Guy Haworth. Data assurance in opaque computations. In H. Jaap Van den Herik and Pieter Spronck, editors, Advances in Computer Games, 12th International Conference (ACG 2009), volume 6048 of Lecture Notes in Computer Science, pages 221–231, Pamplona, Spain. Springer, May 2010. [paper] [bibtex]

The technical details of the formal verification are described in this research paper: