Generalized Strategy Synthesis of Infinite-state Impartial Combinatorial Games via Exact Binary Classification

In game theory, a fundamental class of games is impartial combinatorial games (ICGs). One of the challenging and long-standing problems of ICGs is to compute generalized winning strategies for possibly infinite number of legal states. Recently, Wu et al. proposed an automated method to synthesize generalized winning strategies of infinite-state ICGs. Their method has two major drawbacks: (1) it fails to generate winning formula with large size; and (2) it cannot usually construct the winning strategy even the winning formula is obtained. To tackle the above two drawbacks, in this paper, we propose the problem of exact binary classification and design a partial MaxSAT-based method to this problem. Then, we reduce the synthesis problem of generalized winning strategies of infinite-state ICGs to exact binary classification. The experimental results show that our method is more scalable and effective than Wu et al.'s approach.