conference

QBF Encoding of Generalized Tic-Tac-Toe

Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016), CEUR Workshop Proceedings Vol.1719, pp.14-26 (2016), [peer-reviewed]
Event Date: July 4, 2016

Abstract / 概要

Harary’s generalized Tic-Tac-Toe is an achievement game for polyominoes, where two players alternately put a stone on a grid board, and the player who first achieves a given polyomino wins the game. It is known whether the first player has a winning strategy in the generalized Tic-Tac-Toe for almost all polyominoes except the one called Snaky. $GTTT(p, q)$ is an extension of the generalized Tic-Tac-Toe, where the first player places $q$ stones in the first move and then the players place $q$ stones in each turn. In this paper, in order to attack $GTTT(p, q)$ by QBF solvers, we propose a QBF encoding for $GTTT(p, q)$. Our encoding is based on Gent and Rowley’s encoding for Connect-4. We modify three parts of the encoding: initial condition, move rule and winning condition of the game. The experimental results show that some QBF solvers can be used to solve $GTTT(p, q)$ on $4 \times 4$ or smaller boards.