Concise QBF Encodings for Games on a Grid (extended version)
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Implicit State and Goals in QBF Encodings for Positional Games (extended version)
We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. Our baseline is a QBF encoding with explicit variables for board positions and an explicit representation …
Generic Encodings of Constructor Rewriting Systems
Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewr…
NegationOn Grid Graph Reachability and Puzzle Games
Many puzzle video games, like Sokoban, involve moving some agent in a maze. The reachable locations are usually apparent for a human player, and the difficulty of the game is mainly related to performing actions on objec…
SokobanClassical Planning as QBF without Grounding (extended version)
Most classical planners use grounding as a preprocessing step, reducing planning to propositional logic. However, grounding comes with a severe cost in memory, resulting in large encodings for SAT/QBF based planners. Des…
Fictitious Cross-Play: Learning Global Nash Equilibrium in Mixed Cooperative-Competitive Games
Self-play (SP) is a popular multi-agent reinforcement learning (MARL) framework for solving competitive games, where each agent optimizes policy by treating others as part of the environment. Despite the empirical succes…
Multi-agent Reinforcement Learning