Implicit QBF Encodings for Positional Games

We address two bottlenecks for concise QBF encodings of maker-breaker positional games, like Hex and Tic-Tac-Toe. We improve a baseline QBF encoding by representing winning configurations implicitly. The second improvement replaces variables for explicit board positions by a universally quantified symbolic board position. The paper evaluates the size of these lifted encodings, depending on board size and game depth. It reports the performance of QBF solvers on these encodings. We study scalability up to 19 \(\times \) 19 boards, played in human Hex tournaments.