Solving Two-player Games with QBF Solvers in General Game Playing

Game solving is a relatively less explored area in general game playing. This paper introduces a translation from the Game Description Language GDL to Quantified Boolean Formulas (QBF) that lets us leverage QBF solvers to compute winning strategies in two-player games described in GDL. We implement this approach and measure the computation time needed by state-of-the-art QBF solvers on a range of two-player zero-sum turn-taking games. We introduce a variety of optimizations to the translation and evaluate them experimentally. Our empirical analysis establishes that our proposed approach is suitable for solving small games and can potentially help general game players evaluate endgame positions.