Positional games are a mathematical class of two-player games comprising Tic-tac-toe and its generalizations. We propose a novel encoding of these games into Quantified Boolean Formulas (QBFs) such that a game instance admits a winning strategy for the first player if and only if the corresponding formula is true. Our approach improves over previous QBF encodings of games in multiple ways. First, it is generic and lets us encode other positional games, such as Hex. Second, the structural properties of positional games, together with careful treatment of illegal moves, let us generate more compact instances that can be solved faster by state-of-the-art QBF solvers. We establish the latter fact through extensive experiments. Finally, the compactness of our new encoding makes it feasible to translate realistic game problems. We identify a few such problems of historical significance and put them forward to the QBF community as milestones of increasing difficulty.

翻译：位置游戏是一类数学化的双人游戏，包含井字棋及其推广形式。我们提出了一种将这类游戏编码为量化布尔公式（QBF）的新颖方法，使得游戏实例存在先手获胜策略当且仅当对应公式成立。该方法在多个方面优于以往游戏的QBF编码方案：首先，它具有通用性，可编码如六贯棋等其他位置游戏；其次，通过利用位置游戏的结构特性以及对违规走法的谨慎处理，我们能够生成更紧凑的实例，从而被最先进的QBF求解器更快求解。大量实验验证了这一事实。最后，新编码的紧凑性使得翻译现实游戏问题变得可行。我们甄选了若干具有历史意义的问题，将其作为难度递进的里程碑，推荐给QBF研究社区。