AI Case Study
University of Alberta researchers create a program which cannot lose at checkers using AI planning algorithms
Researchers at the University of Alberta solve the game of checkers by creating a program which cannot lose against any opponent. In fact, the solution to checkers is a game which ends in a draw. This is done using game-tree search.
Public And Social Sector
Education And Academia
"With this paper, we announce that checkers has been weakly solved. From the starting position we have a computational proof that checkers is a draw. The proof consists of an explicit strategy that never loses—the program can achieve at least a draw against any opponent, playing either the black or white pieces. The proof procedure has three algorithm/data components:
* Endgame databases (backward search). Computations from the end of the game back toward the starting position have resulted in a database of 3.9 × 1013 positions (all positions with ≤10 pieces on the board) for which the game-theoretic value has been com- puted (strongly solved)
* Proof-tree manager (forward search). This component maintains a tree of the proof in progress (a sequence of moves and their best responses), traverses it, and generates positions that need to be explored to further the proof’s progress.
* Proof solver (forward search)."
R And D
Core Research And Development
"Checkers (8 × 8 draughts) is a popular game enjoyed by millions of people worldwide, with many annual tournaments and a series of competitions that determine the world champion.... The effort to solve checkers began in 1989, and the computations needed to achieve that result have been running almost continuously since then... With advanced AI algorithms and improved hardware (faster processors, larger memories, and larger disks), it has become possible to push the limits on the type and size of problems that can be solved. Even so, the checkers search space (5 × 1020) represents a daunting challenge for today’s technology.
"The checkers computation pushes the boundary of what can be achieved by search-intensive algorithms. It provides compelling evidence of the power of limited-knowledge approaches to artificial intelligence."
"The solver uses two search programs to evaluate a position. The first program uses Chinook to determine a heuristic value for the position (alpha-beta search to nominal search depths of 17 to 23 ply)... If Chinook does not find a proven result, then a second program is invoked. It uses the Df-pn algorithm, a space-efficient variant of Proof Number search. The search returns a proven, partially proven, or unknown result. Algorithms based on proof numbers maintain a measure of the difficulty of proving a position. This difficulty is expressed as a proof number, a lower bound on the minimum number of positions that need to be explored to result in the position being proven. The algorithm repeatedly expands the tree below the position requiring the least effort to affect the original position (a “best-first” approach). The result of that search is propagated back up the tree, and a new best candidate to consider is determined. Proof number search was specifically invented to facilitate the proving of games. The Df-pn variant builds the search tree in a depth-first manner, requiring less computer storage. A custom compression algorithm was used that allows for rapid localized real-time decompression. This means that the back- ward and forward search programs can quickly extract information from the databases."
"The endgame databases are crucial to solving checkers... The databases contain the win/loss/draw result for a position, not the number of moves to a win/loss... The complete 10-piece databases contain 39 trillion positions."