Possible to solve a combinatorial game with integer programming?

Question

I recently had the idea that it would be neat if it were possible to make a SAT solver play combinatorial games. To start, I'm trying a relatively simple case of solving single-stack Misère Nim through integer programming: there's a fixed limit $L$ with a set of moves $N$, where a move is added to the state each turn. Each player is trying to avoid making the state equal the limit.

I managed to encode this with integer programming with the following system:

• A move at each time $t$ is either played or not played: $0\leq m_{n,t}\leq 1$
• A game is either in progress or over: $0\leq p_t\leq 1$
• The state is between one and the goal: $1\leq s_t \leq L$
• The game starts at state 1 and is in progress, and ends at limit and not in progress: $s_0=1, p_0=1, s_{final}=L, p_{final}=0$
• Exactly one move of the possible moves can be played iff the game is in progress: $\sum_{n\in N}m_{n,t}=p_t$
• The game cannot resume once stopped: $p_t\leq p_{t-1}$
• The current state is the previous state plus the current move: $s_t=s_{t-1}+\sum_{n\in N}nm_{n, t}$

I believe this encoding successfully represents the set of legal games, and enables with minimal additions asking questions like "What is the shortest/longest game" and "Is there a legal game with these constraints".

Where I'm struggling is handling adversarial behavior. I'm not sure how to ask questions like "can this player force a win" via integer programming. I suspect it may not be possible since SAT is in NP but many combinatorial games are in EXP, so the language might not be able to express (cleanly) the idea of an optimal sequence of play. But it may be possible that special cases like Nim (definitely not EXP) yield clever solutions. I can't find any literature on this.

Hence the question: Is it possible to express optimal play for a combinatorial game as integer programming constraints? If so, how? A general solution for zero-sum combinatorial games is preferred if possible, but even just a solution for the special case of (single-stack) Nim would be interesting.

Answer 1

I believe you can't, for many/most combinatorial games. In particular, I believe optimal play for two-player combinatorial games is often a PSPACE-complete problem (sometimes a EXP-complete problem), while a SAT solver can only express NP problems (and a polynomial-time algorithm equipped with ability to call a SAT solver can only solve problems in $P^{NP}$). Since it is believed that PSPACE is much bigger than NP (or $P^{NP}$), it is unlikely that a SAT solver will be enough to solve all such game problems.

See, e.g., Playing Games with Algorithms: Algorithmic Combinatorial Game Theory, Erik D. Demaine and Robert A. Hearn, Games of No Chance 3, volume 56, pages 3-56, 2009; or David Eppstein's page, or Wikipedia's page (also here and here).

Another way to think about it is that reasoning about adversarial play often involves formulas of the form $\forall x_1 \exists y_1 \forall x_2 \exists y_2 \forall x_3 \exists y_3 \cdots \varphi(x_1,y_1,\cdots)$. Here the $x_1,x_2,\dots$ variables represent one player's moves, and the $y_1,y_2,\dots$ variables represent the other player's moves. In general, such formulas are PSPACE-complete to solve: see TQBF. Therefore, it is unlikely that they can be solved with a SAT solver (or an ILP solver).