论文标题
位置游戏和QBF：抛光编码
Positional Games and QBF: A Polished Encoding
论文作者
论文摘要
位置游戏是包括TIC-TAC-TOE及其概括的两人游戏的数学类别。我们将这些游戏编码的小说编码为量化的布尔公式（QBF），以便在且仅当相应的公式为真时，游戏实例就可以接受第一个玩家的胜利策略。我们的方法通过多种方式改进了游戏的QBF编码。首先，它是通用的，让我们可以编码其他位置游戏，例如十六进制。其次，位置游戏的结构属性以及对非法动作的仔细处理，让我们生成更紧凑的实例，可以通过最新的QBF求解器更快地解决。我们通过广泛的实验来建立后一种事实。最后，我们新编码的紧凑性使翻译现实的游戏问题是可行的。我们确定了一些具有历史意义的问题，并将其提出QBF社区是增加难度的里程碑。
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.
