Kai Liang
Abstract
This study applies finite automata to the automatic solving of a variety of combinatorial games. For games whose positions and moves can be represented as regular languages and their operations, we design a two-stage automatic solving algorithm: first, construct a candidate finite automaton to determine the - and -positions, and then perform rigorous formal verification on this automaton; once verified, a complete solution of the game is obtained. For partizan octal games, we introduce a generalized misère quotient, overcoming the limitation that traditional theory applies only to impartial games. Using the above algorithm, we successfully solve the majority of two-digit partizan octal games, and based on these results, we propose a partizan version of Guy's conjecture. We also successfully solve a considerable number of partizan octal games under misère play, and give a conjecture on the structure of those games exhibiting ``algebraic periodicity'' among them. For Kotzig's nim, we resolve the most important related conjecture: we prove that the outcomes and SG values are periodic under both normal and misère play (including their partizan versions). Our algorithm successfully solves several small-scale cases, including misère play and partizan versions. This study pioneers a new theoretical tool and algorithmic paradigm for the automatic solving of combinatorial games, and has broad prospects for further extension and application in the field of combinatorial game theory.