QBF Encoding of Generalized Tic-Tac-Toe

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 × 4 or smaller boards.

Introduction

In recent years it has been getting a more common approach to use SAT solvers to tackle some sort of hard problems for which no polynomial-time algorithm is known. Those problems include cryptanalysis [ 22, 26 ] and mathematical problems such as the Erdo˝s discrepancy conjecture [ 17 ]. Still there are even harder problems in the real world to which SAT solvers cannot apply. The successful development of solvers for the QBF satisfiability problem (QBF solvers) [ 11, 14, 21 ] such as DepQBF [ 19, 18 ], RAReQS [ 25 ] and GhostQ [ 16 ] allows us to use them to attack PSPACE problems. Typical PSPACE problems are to decide whether a player has a winning strategy in two-player perfect information games. Particular instances of these games can be solved by reducing the game rules and a game position into a QBF and giving it to a QBF solver.

A trivial example of a two-player perfect information game is Tic-Tac-Toe (TTT), where two players alternately put a stone on a cell in the 3 × 3 board and the player who occupies three consecutive cells constituting a line will win. A generalization of TTT is known as mnk-Game, where players aim at achieving a line of length k on the m × n-board. While the original TTT can be solved easily, it is known that to decide the winner of mn5-Game for a given position is PSPACE-complete [ 23 ]. Even when the game position of an instance is restricted to be blank, it has been open if the first player has a winning strategy in mn5Game except for limited values of m and n [ 28 ].

Harary’s generalized Tic-Tac-Toe (HTTT) is another variant [ 8 ]. The goal of HTTT is to achieve a given polyomino, i.e., a group of cells connected to each other with edges, rather than a line. Fig. 1 gives an example of a game position of HTTT. The first and second players’ stones are colored black and white, respectively, and the first player has won the game, because the four black stones numbered 1, 2, 4 and 5 form the target shape shown in the bottom left corner. Note that any rotation of the target polyomino and its reflection are admitted. HTTT has already been solved for all polyominoes on an arbitrary size board except cases of Snaky (Fig. 2) [ 8, 9 ]. Snaky is the name of a polyomino consisting of 6 cells. When the target is Snaky and the board dimension is 8 × 8 or smaller, it is known that no player has a winning strategy [ 7 ]. However, it is open for bigger boards. On the other hand, if the first player gets one additional stone at the initial position, he/she can certainly win [ 7, 10 ].

Diptarama et al. [ 4, 5 ] have proposed a further generalization, which we denote by GTTT(p, q), where the first player puts q stones at the first turn and then the two play p stones at each of their turns afterwards. Hence, GTTT(1, 1) is HTTT and GTTT(1, 2) corresponds the situation where the first player has a handicap stone at the beginning of a game. They showed that the first player will win in GTTT(2, 2) and the second player will win in GTTT(2, 1). Diptarama et al. [ 3 ] reported that in some cases QBF solvers can solve GTTT(p, q) that encoded by a tool called Toss [ 15, 27 ] faster than the proof number search [ 1 ]. Therefore, the QBF approach seems to be hopeful to tackle GTTT(p, q), including HTTT for Snaky. In order to evaluate the potential of the QBF approach against GTTT(p, q), we propose a QBF encoding of GTTT(p, q) and apply QBF solvers to it in this paper. Our QBF encoding is based on Gent and Rowley’s encoding for the game called Connect-4. We modify their encoding for the initial position, players’ move, and winning condition. We submitted 180 instances from GTTT(p, q) as benchmarks to QBFEVAL’16. This paper shows and analyses experimental results on those instances, where only instances with small board and target shape were solved. It still remains open whether the first player has a winning strategy in HTTT for Snaky on the 9 × 9 board. The instances are available at www.shino.ecei.tohoku.ac.jp/~diptarama/gttt_qbf.html. In this section, we will describe how to encode GTTT(p, q) into a QBF which holds true if and only if the first player has a winning strategy. It is easy to modify our formula for checking whether the second player can win. We modify the QBF encoding of the Connect-4 game proposed by Gent and Rowley [ 6 ], and define a new encoding for GTTT(p, q). First, we describe notation that used in variables and clauses. Next, we describe variables and quantifiers that are used in the GTTT(p, q) encoding. Last, we show clauses that are used in the GTTT(p, q) encoding. Throughout this paper we call the first player Black and the second player White. Let W and H be the width and height of the game board, respectively. The maximum number Z of turns of the game in GTTT(p, q) is bounded by Z = ⌊(W H − q)/p⌋ + 1, because the first player places q stones at the first move and then both players place p stones respectively.

Next, similarly to the Connect-4 encoding, we define illegal moves in the game as cheats. We classify illegal moves into 4 categories; (1) the player places more stones than the number of stones that the player should place in one move, (2) the player places less stones than the number of stones that the player should put in one move, (3) the player places a stone on an occupied cell, and (4) the first player puts his/her first stone outside a specific area. The fourth kind of a cheat is not regarded illegal in a usual game play, but in our encoding, we force the first stone to be put in a special area to reduce the number of moves to be considered by breaking symmetries. The number of cheats in category a is denoted by Ca for a ∈ {1, 2, 3, 4}. Then, C1 = Wp+H1 at the first turn and C1 = Wq+H1 otherwise. C2 = Wp−H1 at the first turn and C2 = Wq−H1 otherwise. Moreover, C3 = W H and C4 = 1.

Last, the target shapes that both players try to achieve in a game are defined as follows. We represent a polyomino’s shape as a tuple of relative coordinates of the cells s = ((sx1 , sy1 ), (sx2 , sy2 ), . . . , (sxk , syk )), where mini sxi = mini syi = 0 and k is the number of cells of the polyomino. We define |s|W = maxi sxi + 1 and |s|H = maxi syi + 1, which denote the width and height of the target shape, respectively. Since all of the 90, 180, 270 degree rotations and their reflections of a polyomino are admitted as a target, the target shapes of GTTT(p, q) are represented as a set S = {s1, s2, . . . , s|S|}, where |S| ≤ 8. If the polyomino is symmetric, |S| can be smaller than 8. For example, Fig. 3 shows the target shapes when the target polyomino is Tippy (see Fig. 2). By using the above parameters, we define variables used in the QBF encoding of GTTT(p, q) as follows. The range of each of the parameters below is as follows: 1 ≤ x ≤ W , 1 ≤ y ≤ H, 1 ≤ a ≤ 4, 1 ≤ c ≤ Ca, and 1 ≤ s ≤ |S|. Moreover, 1 ≤ z ≤ Z + 1 for gameover z and occupied z,x,y, and 1 ≤ z ≤ Z for the rest. 1. blackwin, whitewin, and draw : true iff Black wins, White wins, or draws, respectively. 2. blackwinz and whitewinz: true iff Black or White wins at turn z, respectively. 3. gameover z: true iff game is over at turn z. 4. occupied z,x,y: true iff the cell at coordinates (x, y) is occupied by either a black or white stone before move z has been made. 5. black z,x,y and whitez,x,y: true iff there is a black or white stone on the cell at coordinates (x, y) after move z has been made, respectively. 6. blackcheatsz,a,c and whitecheatsz,a,c: true iff Black or White respectively does an illegal move numbered c in category a at turn z. 7. blackcheat z and whitecheat z: true iff Black or White respectively does any of illegal moves at turn z. 8. blackshapez,i,x,y and whiteshapez,i,x,y: true iff Black or White respectively achieves a target shape si on coordinates (x, y) as origin at turn z. 9. blackmovez,x,y and whitemovez,x,y: true iff Black or White respectively places a stone on a cell at coordinates (x, y) at turn z.

Quantifiers in QBF encoding of GTTT(p, q) are defined for each turn. ∃.(blackwin, whitewin, draw , gameover 1, occupied 1,1,1, . . . , occupied 1,W,H ) ∃.(blackmove1,1,1, blackmove1,1,2, . . . , blackmove1,W,H ) ∃.(gameover 2, occupied 2,x,y, black 1,x,y, white1,x,y, blackcheat 1, whitecheat 1, . . .) ∀.(whitemove2,1,1, whitemove2,1,2, . . . , whitemove2,W,H ) ∃.(gameover 3, occupied 3,x,y, black 2,x,y, white2,x,y, blackcheat 2, whitecheat 2, . . .) . .

. ∃.(blackmoveZ,1,1, blackmoveZ,1,2, . . . , blackmoveZ,W,H ) ∃.(gameover Z+1, occupied Z+1,x,y, black Z,x,y, whiteZ,x,y, . . .)

First we introduce variables blackwin, whitewin, draw , gameover 1, and occupied 1,x,y with the existential quantifier, which will be forced to be 1, 0, 0, 0, and 0, respectively, in the body CNF. Then for each turn z with 1 ≤ z ≤ Z, we place “move” variables blackmovez,i,j and whitemovez,i,j with ∃ for blackmovez,i,j and ∀ for whitemovez,i,j . After those move variables, we use ∃ for “state” variables gameover z+1, occupied z+1, blackwinz, whitewinz, black z,x,y, whitez,x,y, blackcheatsz,a,c, whitecheatsz,a,c, blackcheat z, whitecheat z, blackshapez,s,x,y and whiteshapez,s,x,y. These variables are used to express the board state after each player has ended his turn.

Note that if we want to determine whether White wins or not, we switch quantifiers for the move variables; ∀ for blackmovez,i,j and ∃ for whitemovez,i,j . 2.3

Clauses We now describe the body CNF used in our GTTT(p, q) encoding. Some of the formulas presented below are not conjunctions of clauses, which is only for readability. Converting them into a CNF is easy and does not increase the size of the formula significantly.

There are mainly three differences from the encoding of Connect-4. (1) All cells are empty at the initial condition in GTTT(p, q). (2) A move in GTTT(p, q) is defined as placing stones on any empty cell on the board, instead of dropping stones in any column. (3) The winning condition in GTTT(p, q) is to achieve any of 0, 90, 180, 270 degrees rotation or reflection of the given polyomino.

We also implement the winning condition for torus board as an extension of the game in our encoding.

The encoding for GTTT(p, q) is the conjunction of the formulas described below. First, we will describe the clauses that are different from the encoding of Connect-4. Note that we only show clauses for Black, because ones for White can be obtained symmetrically.

Initial Condition There is no stone on any cell at the initial condition.

W H ^ ^ (¬occupied 1,x,y) x=1 y=1 Move rule There are two modifications for the move rule in GTTT(p, q) encoding. First, the clauses for the move rule are modified from dropping the stone to the board, into placing the stone on the board. Second, we extend cheat clauses so that the player can place more than one stone for one move in GTTT(p, q). We also add cheat rules when a player places a stone on an occupied cell. 1. The move in GTTT(p, q) is defined as placing a stone on an empty cell of the board. Therefore, if a cell is empty then a black stone will be on the cell iff Black places a stone on the cell.

⌊ Z2 ⌋ W H ^

^ ^ (gameover 2z ∨ (¬occupied 2z,x,y =⇒ ¬black 2z,x,y)) z=1 x=1 y=1 3. Let B be the set of all cells in the board, and Bv be the set of all vcombinations of B. Let nz be the number of stones that Black can place at turn z. Then Mz = nzB+1 is the collection of nz + 1 cells that are filled by black stones when Black places nz + 1 stones at turn z. Let f : Mz → {1, . . . , |Mz|} be an injection which maps each m ∈ Mz to an unique id f (m) of the move rule in category 1.

⇐⇒ blackcheats2z−1,1,f(m))) 5. Black does illegal moves of category 3 iff Black places a stone on an occupied cell, where the function h(x, y) = W ·(y − 1) + x maps each coordinates (x, y) to an unique id of the move rule in category 3. 6. Black has cheated iff he did one of the illegal moves. Winning condition For a given polyomino, we calculate all rotations and reflections of the polyomino and then use them as target shapes for winning condition. Not only a polyomino, but any shape can also be used in this encoding, such as straight line in connect(m, n, k, p, q) [ 29 ] or wild polyomino [ 24 ]. Furthermore, we also implement winning condition for torus board in our encoding. 1. Black achieves a target shape iff there are black stones on the board that form the target shape.

Z |S| W −|si|W +1 H−|si|H+1 ^ ^ ^ ^ For torus board, let mod (u, v) = ((u − 1) mod v) + 1. We connect leftmost cells with rightmost cells and top cells with bottom cells when we check whether or not a target shape is achieved by Black.

k Z |S| W H ^ ^ ^

^ (gameover z ∨ (( ^ black z,mod(x+sixj ,W ),mod(y+siyj ,H)) z=1 i=1 x=1 y=1 j=1

⇐⇒ blackshapez,i,x,y)) 2. If Black has not cheated, then Black wins the game at turn z iff he achieves a target shape or White cheats. We use 1 ≤ x ≤ W , 1 ≤ y ≤ H for torus board.

Z ^ (gameover z ∨ (¬blackcheatsz =⇒ z=1

S W −|si|W +1 H−|si|H+1 ((_ _ _ i=1 x=1 y=1

blackshapez,i,x,y ∨ whitecheatsz) ⇐⇒ blackwinz))) 3. Black cannot win if he has cheated, and he cannot cheat at White turn.

Z ^ (gameover z ∨ (blackcheatsz =⇒ ¬blackwinz)) ∧ ^ (¬blackcheats2z) z=1 z=1 ⌊ Z2 ⌋ 4. Black wins if he wins the game at any turn.

Z ( _ (¬gameover z ∧ blackwinz) ⇐⇒ blackwin) z=1 Symmetry breaking We use three types of clauses for symmetry breaking, depending on the type of the board. The first clauses are symmetry breaking for the general board, the second clauses for square board (W = H), and the third clauses for torus board. 1. On general board, Black must place his first stone on the top left side rectangle of the board.

⌈ W2 ⌉ ⌈ H2 ⌉ ⌈ W2 ⌉ ⌈ H2 ⌉ (gameover 1 ∨ ( ^ ^ ¬blackmove1,x,y ⇐⇒ blackcheat 1,4,1))

x=1 y=1 On square board, Black must place his first stone on the top left side triangle of the board.

(gameover 1 ∨ ( ^ ^ ¬blackmove1,x,y ⇐⇒ blackcheat 1,4,1))

x=1 y=x On torus board, Black must place his first stone on the center of the board.

(gameover 1 ∨ (¬blackmove1,⌈ W2 ⌉,⌈ H2 ⌉ ⇐⇒ blackcheat 1,4,1))

Next, we will describe the clauses of the GTTT(p, q) encoding that are the same as the Connect-4 encoding.

Board management We manage the cells of the board by the following clauses. 1. Any cell of the board cannot be occupied by both black stone and white stone simultaneously.

Z W H ^ ^ ^ (gameover z ∨ ¬black z,x,y ∨ ¬whitez,x,y) z=1 x=1 y=1 2. Any cell of the board is occupied if either a black stone or a white stone is placed at the previous turn.

Z W H ^ ^ ^ (gameover z ∨ ((black z,x,y ∨ whitez,x,y) ⇐⇒ occupied z+1,x,y)) z=1 x=1 y=1 3. If a cell is occupied by a black stone, then the cell is also occupied by black stone at the next turn.

Z−1 W H ^ ^ ^ (gameover z ∨ (black z,x,y =⇒ black z+1,x,y)) z=1 x=1 y=1 Others 1. For any turn z, if the game has been already over, then the game is also over at the next turn. Also if the game is not over, then the game is over at next turn iff Black or White wins at this turn.

Z−1 ^ (gameover z =⇒ gameover z+1) z=1

Z−1 ∧ ^ (¬gameover z =⇒ ((blackwinz ∨ whitewinz) ⇐⇒ gameover z+1)) z=1 2. Black cannot win after the game has over.

Z−1 ^ (gameover z =⇒ ¬blackwinz) z=1 3. We set blackwin as a clause if we want to check whether Black can win the game or not. Exactly one of blackwin, whitewin, and draw must be true. The game finishes draw iff the game is not over at turn Z + 1.

(blackwin) ∧(¬gameover 1) ∧(blackwin ∨ whitewin ∨ draw ) ∧(¬blackwin ∨ ¬whitewin) ∧ (¬blackwin ∨ ¬draw ) ∧ (¬whitewin ∨ ¬draw ) ∧(¬gameover Z+1 ⇐⇒ draw ) We conducted experiments by solving GTTT(p, q) by using QBF solvers. We generated 84 (= 3 × 7 × 2 × 2) instances from GTTT(p, q) on 3 × 3 board, which is the combination of the following parameters. The values of p and q for 1 ≤ q ≤ p ≤ 2, 7 polyominoes of 2–4 cells aside Skinny (see Fig. 2), 2 types of board; regular and torus board, and instances for Black and White. We also generated 96 (= 3 × 8 × 2 × 2) instances from GTTT(p, q) on 4 × 4, with the same parameters as the 3 × 3 board, but we used all 2–4 cell polyominoes including Skinny. Table 1 shows some statistics of the instances that are used in the experiments.

We used a computer with Intel Xeon CPU E5-2609 8 cores 2.40GHz, 256GB memory, and Debian Wheezy OS as experimental environment. We used DepQBF [ 18 ], RAReQS [ 12 ], GhostQ [ 16 ], and MPIDepQBF [ 13 ] as solvers and bloqqer [ 2 ] for preprocessing. We use 8 cores when running the MPIDepQBF.

Fig. 4 and Fig. 5 show the running time of each solver on solving the instances of GTTT(p, q) on 3 × 3 and 4 × 4 boards, respectively. Notice that the point on 10 seconds on Fig. 4 (resp. 1000 seconds on Fig. 5) means that the solver solves the instances in 10 (resp. 1000) seconds or more. From Fig. 4 we can see that DepQBF solves the instances of GTTT(p, q) on 3 × 3 board faster than the other solvers. We can also see that preprocessing is not effective for DepQBF and depqbf ghostq rareqs 30 40 50 Number of solved instances

mpidepqbf bloqqer-depqbf bloqqer-ghostq 60 70

80 bloqqer-rareqs bloqqer-mpidepqbf GhostQ from this result. On the other hand, from Fig. 5, MPIDepQBF with preprocessing is the fastest solver on solving the instances of GTTT(p, q) on 4 × 4 board. The preprocessing by using bloqqer is effective on DepQBF and MPIDepQBF in this case. The detailed number of instances and its result (SAT or UNSAT) are shown in Table. 2.

From these experimental results, we can conclude that the QBF solvers can solve most instances of GTTT(p, q) on 3 × 3 and 4 × 4 within 1000 seconds. Different to the results in [ 11, 21 ], DepQBF and MPIDepQBF can solve most of the instances faster than other solvers. This indicates that the QBF solving algorithm of DepQBF is more suitable to solve GTTT(p, q) encoding than other solvers. We can also see that parallelization is more effective when solving GTTT(p, q) encoding on 4 × 4 board. However, a better encoding and faster solver are needed in order to solve the instances of GTTT(p, q) on larger board and polyomino in less than 1000 seconds. Therefore, improving the encoding and the solvers are needed in order to solve Snaky on HTTT by using QBF solver. 4

Conclusion

We have proposed a QBF encoding of an extension GTTT(p, q) of Harary’s generalized Tic-Tac-Toe. However, by our encoding, existing QBF solvers could not solve the open problem on HTTT, whether the first player has a winning strategy to achieve a Snaky on the 9 × 9 board, that has 616578 variables, 1557653 clauses, and 80 quantifier alternations in its instance, which are much bigger than the instances on 4 × 4 board. Our encoding technique is rather naive and easily understandable, so there remains a lot of room to improve. For example, our encoding contains many redundant clauses. Some of them would help QBF solvers search, but we did not examine which of them have a real positive effect. Moreover, although our encoding did not consider an incremental QBF solving [ 20 ], the encoding might be solved in incremental way because we can use the knowledge from the result on solving an instance of smaller board to solve an instance of larger board. Therefore, the encoding optimization for incremental QBF solving can be considered as a future work. We hope our experimental results and analysis help to improve QBF solvers and the open problem will be solved by a QBF approach by an even more elaborated QBF solver with a more sophisticated encoding in the future.

Acknowledgment

This work is supported by Tohoku University Divison For Interdisciplinary Advance Research and Education. We thank Charles Jordan for his advises on writing this paper.

References

1. Allis , L., van der Meulen , M., van den Herik, H.J.: Proof-number search . Artificial Intelligence 66 ( 1 ) ( 1994 ) 91 - 124

2. Biere , A. , Lonsing , F. , Seidl , M. : Blocked clause elimination for QBF . In: CADE' 11 . ( 2011 ) 101 - 115

3. Diptarama , Ishiguro, Y. , Narisawa , K. , Shinohara , A. , Jordan , C. : Solving generalized tic-tac-toe by using QBF solver . In: Proceedings of Game Programming Workshop 2015 . Volume 2015 . (oct 2015 ) 154 - 161 (In Japanese).

4. Diptarama , Narisawa, K. , Shinohara , A. : Extension of generalized tic-tac-toe: p stones for one move . IPSJ Journal 55 ( 11 ) (nov 2014 ) 2344 - 2352 (In Japanese).

5. Diptarama , Narisawa, K. , Shinohara , A. : Drawing strategies for generalized tictac-toe (p, q) . AIP Conference Proceedings 1705 ( 2016 )

6. Gent , I.P. , Rowley , A. : Encoding connect-4 using quantified boolean formulae . 2nd Intl. Work. Modelling and Reform . CSP ( 2003 ) 78 - 93

7. Halupczok , I. , Schlage-Puchta , J.C. : Achieving snaky . Electronic Journal of Combinatorial Number Theory 7 ( 2007 ) G02

8. Harary , F. : Achievement and avoidance games for graphs . Ann. Discrete Math 13 ( 1982 ) 111 - 120

9. Harary , F. : Achieving the skinny animal . Eureka 42 ( 1982 ) 8 - 14

10. Ito , H. , Miyagawa , H.: Snaky is a winner with one handicap . In: Proceedings of 8th Hellenic European Conference on Computer Mathematics and its Applications (HERCMA 2007 ). ( 2007 ) 25 - 26

11. Janota , M. , Jordan , C. , Klieber , W. , Lonsing , F. , Seidl , M. , Van Gelder , A. : The QBFGallery 2014 : The QBF competition at the FLoC olympic games . Journal on Satisfiability, Boolean Modeling and Computation 9 ( 2016 ) 187 - 206

12. Janota , M. , Klieber , W. , Marques-Silva , J. , Clarke , E.: Solving QBF with counterexample guided refinement . In: SAT' 12 . ( 2012 ) 114 - 128

13. Jordan , C. , Kaiser , L. , Lonsing , F. , Seidl , M.: MPIDepQBF: Towards parallel qbf solving without knowledge sharing . In: Theory and Applications of Satisfiability Testing-SAT 2014 . Springer ( 2014 ) 430 - 437

14. Jordan , C. , Seidl , M. : QBF gallery 2014 ( 2014 )

15. Kaiser , L. , Stafiniak , L. : Playing structure rewriting games . In: AGI' 10 . ( 2010 )

16. Klieber , W. , Sapra , S. , Gao , S. , Clarke , E.: A non-prenex, non-clausal QBF solver with game-state learning . In: Theory and Applications of Satisfiability TestingSAT 2010 . Springer ( 2010 ) 128 - 142

17. Konev , B. , Lisitsa , A. : A SAT attack on the Erd˝os discrepancy conjecture . In: Theory and Applications of Satisfiability Testing-SAT 2014 . Springer ( 2014 ) 219 - 226

18. Lonsing , F. , Bacchus , F. , Biere , A. , Egly , U. , Seidl , M. : Enhancing search-based QBF solving by dynamic blocked clause elimination . In: Logic for Programming , Artificial Intelligence, and Reasoning , Springer ( 2015 ) 418 - 433

19. Lonsing , F. , Biere , A. : DepQBF: A dependency-aware QBF solver . Journal on Satisfiability, Boolean Modeling and Computation 7 ( 2010 ) 71 - 76

20. Lonsing , F. , Egly , U. : Incremental QBF solving . In: Principles and Practice of Constraint Programming-CP 2014 . Springer ( 2014 ) 514 - 530

21. Lonsing , F. , Seidl , M. , Van Gelder , A. : The QBF gallery: Behind the scenes . arXiv preprint arXiv:1508.01045 ( 2015 )

22. Mironov , I. , Zhang, L.: Applications of SAT solvers to cryptanalysis of hash functions . In: Theory and Applications of Satisfiability Testing-SAT 2006 . Springer ( 2006 ) 102 - 115

23. Reisch , S. : Gobang ist PSPACE-vollsta¨ndig . Acta Inf . 13 ( 1980 ) 59 - 66

24. Sieben , N.: Wild polyomino weak (1, 2)-achievement games . Geombinatorics 13 ( 4 ) ( 2004 ) 180 - 185

25. Sieben , N.: Polyominoes with minimum site-perimeter and full set achievement games . European Journal of Combinatorics 29 ( 1 ) ( 2008 ) 108 - 117

26. Soos , M. , Nohl , K. , Castelluccia , C. : Extending SAT solvers to cryptographic problems . In: Theory and Applications of Satisfiability Testing-SAT 2009 . Springer ( 2009 ) 244 - 257

27. Toss Team: Toss http://toss.sourceforge.net/.

28. Uiterwijk , J.W.H.M. , van den Herik, H.J.: The advantage of the initiative . Inf. Sci . 122 ( 1 ) ( 2000 ) 43 - 58

29. Wu , I.C. , Huang , D.Y.: A new family of k-in-a-row games . In: Proceedings of Advances in Computer Games . ( 2006 ) 180 - 194