The King-Pawn Chess Game: A Logical Analysis Using Satisfiability Modulo Theories

Abstract

Chess analysis in the past several decades has been dominated by the ever-improving fields of machine learning and artificial intelligence. This project approaches chess analysis from an entirely different perspective, focusing on logically and systematically defining the game in order to uncover truths about the game at large, as well as generating positions such as stalemates, wins, and Zugzwangs. Using Z3, a modern SMT solver, we are able to generate and enumerate different configurations of the chess board, thereby giving us insights into the game of chess. The success of this project in producing tangible and meaningful results from an SMT solver based analysis of chess suggests that SMT solvers should be applied further to the analysis of the game of chess, as well as to other strategic two-player games. While artificial intelligence may be the best method for winning these games, SMT solvers offer insights into the positions and the logic of chess, allowing for highly-precise position analysis, enumeration, and generation.