位置博弈与 QBF：一种精炼编码
Positional Games and QBF: A Polished Encoding
AI总结：
本文提出一种将位置博弈编码为 QBF 的通用精炼方法，利用博弈结构和非法着法处理生成更紧凑实例，实验证明其求解更快，并给出难度递增的现实问题里程碑。
摘要：
位置博弈是一类双人数学博弈，包含井字棋及其各种推广。我们提出一种将这些博弈编码为量化布尔公式（QBF）的新颖方法，使得一个博弈实例中先手拥有获胜策略，当且仅当相应公式为真。我们的方法在多个方面改进了以往博弈的 QBF 编码。首先，它具有通用性，使我们能够编码其他位置博弈，例如 Hex。其次，位置博弈的结构性质连同对非法着法的谨慎处理，使我们能够生成更紧凑的实例，这些实例可由最先进的 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
