Concise QBF Encodings for Games on a Grid
正确和高效地将2player游戏编码为QBF是一项挑战性且容易犯错误的任务。为了在gridboard游戏(如Tic-Tac-Toe、 Connect-4、Domineering、 Pursuer-Evader和突破)上 concise 和一致的编码，我们引入了Board-game Domain Definition Language (BDDL), inspired by the success of PDDL in the planning domain。我们提供了高效的BDDL到QBF的翻译，编码有限制深度的获胜策略的存在。我们的 lift 编码将牌位符号化，并允许对符号化的牌位位置的 conditions、效果和获胜配置的简明定义。编码的大小在输入模型和考虑深度上线性增长。为了证明这种通用方法的可行性，我们使用QBF求解器计算多个已知游戏的获胜策略的关键深度。对于多个游戏，我们的工作提供了QBF编码的第一个实现。与基于SAT的计划验证不同，验证基于QBF的获胜策略很困难。我们展示了如何使用QBF证书和交互游戏 play 来验证获胜策略。
Encoding 2-player games in QBF correctly and efficiently is challenging and error-prone. To enable concise specifications and uniform encodings of games played on grid boards, like Tic-Tac-Toe, Connect-4, Domineering, Pursuer-Evader and Breakthrough, we introduce Board-game Domain Definition Language (BDDL), inspired by the success of PDDL in the planning domain. We provide an efficient translation from BDDL into QBF, encoding the existence of a winning strategy of bounded depth. Our lifted encoding treats board positions symbolically and allows concise definitions of conditions, effects and winning configurations, relative to symbolic board positions. The size of the encoding grows linearly in the input model and the considered depth. To show the feasibility of such a generic approach, we use QBF solvers to compute the critical depths of winning strategies for instances of several known games. For several games, our work provides the first QBF encoding. Unlike plan validation in SAT-based planning, validating QBF-based winning strategies is difficult. We show how to validate winning strategies using QBF certificates and interactive game play.
https://arxiv.org/abs/2303.16949
https://arxiv.org/pdf/2303.16949