[Toss-devel] Solving Games using QBF Solvers

 [Toss-devel] Solving Games using QBF Solvers From: Lukasz Kaiser - 2013-06-08 21:34:36 ```Hi. I just commited a first version of TossServer that allows to generate QBF formulas that are equivalent to the existence of a winning strategy in at most n moves. For example ./TossServer -f examples/Tic-Tac-Toe.toss -qbf 9 generates a formula saying "player 0 wins in at most 9 moves". The generated file is in qdimacs format, so it can be piped into any standard QBF solver. For example one can use depqbf http://lonsing.github.io/depqbf/ and, predictably, issuing the following command ./TossServer -f examples/Tic-Tac-Toe.toss -qbf 9 | ./depqbf results in "UNSAT" (in under 2s). To check whether the other player (player1) can win in a given number of moves use -N, e.g. ./TossServer -f examples/Tic-Tac-Toe.toss -qbf -9 | ./depqbf which also reports UNSAT in this case (as it is a tie). For now, the qbf generation work only for a limited class of games. The game must be 2-player, strictly alternating - so only 2 locations, player0 moving only in the first one, player1 only in the second one. Moreover, the use of _new, _del, and _opt in rules is not yet supported (so no +,-,? in the structure syntax in rules for now), and payoffs must be written either as :(phi) or as :(phi1) - :(phi2), because for now "wins" means "gets payoff >0" and this condition must translate into a formula. Additionally, all fluents in rules must have arity 1 for now. Even with these limitations, there are quite a few games for which this works quite well. In particular, all ConnectX variants work, and one can also translate Pawns (Pawn-Whopping) but *without en passant* (as it uses _old in the rule) and with re-written payoffs to make clear who can and who cannot move at the end. The translation get slow for bigger board sizes and many moves, but it is not a limiting factor for now. Of course actually solving the generated file is another question. A few first checks seem to indicate that depqbf is one of the best solvers on this class of instances. It can solve Connect4 on a 4x4 board (16 moves) in around two minutes, and 2x8 pawns (8 moves suffice for black) in more or less a similar time. Bigger boards with more moves are harder of course, but this could still be an interesting way to check for winning in endgames. Moreover, it is trivial to adapt the formula to questions like "is there some placement of pawns such that black wins in 2 moves from here" or things like that. And there is absolutely no symmetry breaking for now - other works indicate that breaking symmetry could help QBF solvers a lot. Best! Lukasz ```

 [Toss-devel] Solving Games using QBF Solvers From: Lukasz Kaiser - 2013-06-08 21:34:36 ```Hi. I just commited a first version of TossServer that allows to generate QBF formulas that are equivalent to the existence of a winning strategy in at most n moves. For example ./TossServer -f examples/Tic-Tac-Toe.toss -qbf 9 generates a formula saying "player 0 wins in at most 9 moves". The generated file is in qdimacs format, so it can be piped into any standard QBF solver. For example one can use depqbf http://lonsing.github.io/depqbf/ and, predictably, issuing the following command ./TossServer -f examples/Tic-Tac-Toe.toss -qbf 9 | ./depqbf results in "UNSAT" (in under 2s). To check whether the other player (player1) can win in a given number of moves use -N, e.g. ./TossServer -f examples/Tic-Tac-Toe.toss -qbf -9 | ./depqbf which also reports UNSAT in this case (as it is a tie). For now, the qbf generation work only for a limited class of games. The game must be 2-player, strictly alternating - so only 2 locations, player0 moving only in the first one, player1 only in the second one. Moreover, the use of _new, _del, and _opt in rules is not yet supported (so no +,-,? in the structure syntax in rules for now), and payoffs must be written either as :(phi) or as :(phi1) - :(phi2), because for now "wins" means "gets payoff >0" and this condition must translate into a formula. Additionally, all fluents in rules must have arity 1 for now. Even with these limitations, there are quite a few games for which this works quite well. In particular, all ConnectX variants work, and one can also translate Pawns (Pawn-Whopping) but *without en passant* (as it uses _old in the rule) and with re-written payoffs to make clear who can and who cannot move at the end. The translation get slow for bigger board sizes and many moves, but it is not a limiting factor for now. Of course actually solving the generated file is another question. A few first checks seem to indicate that depqbf is one of the best solvers on this class of instances. It can solve Connect4 on a 4x4 board (16 moves) in around two minutes, and 2x8 pawns (8 moves suffice for black) in more or less a similar time. Bigger boards with more moves are harder of course, but this could still be an interesting way to check for winning in endgames. Moreover, it is trivial to adapt the formula to questions like "is there some placement of pawns such that black wins in 2 moves from here" or things like that. And there is absolutely no symmetry breaking for now - other works indicate that breaking symmetry could help QBF solvers a lot. Best! Lukasz ```