Automatic Synthesis of Generalized Winning Strategy of Impartial Combinatorial Games

One of the challenging problems of impartial combinatorial games (ICGs) is to construct generalized winning strategies for possibly infinitely many states. In this paper, we investigate synthesizing generalized winning strategies for ICGs. To this end, we first propose a logical framework to formalize ICGs based on linear integer arithmetic. We then propose an approach to generating the winning strategy for ICGs. Experimental results on several games demonstrate that our approach is effective in most of these games.