Positional Games and QBF: The Corrective Encoding

Abstract

Positional games are a mathematical class of two-player games comprising Tic-tac-toe and its generalizations. We propose a novel encoding of these games into Quantified Boolean Formulas (QBFs) such that a game instance admits a winning strategy for first player if and only if the corresponding formula is true. Our approach improves over previous QBF encodings of games in multiple ways. First, it is generic and lets us encode other positional games, such as Hex. Second, structural properties of positional games together with a careful treatment of illegal moves let us generate more compact instances that can be solved faster by state-of-the-art QBF solvers. We establish the latter fact through extensive experiments. Finally, the compactness of our new encoding makes it feasible to translate realistic game problems. We identify a few such problems of historical significance and put them forward to the QBF community as milestones of increasing difficulty.

1 Introduction

In a positional game [3, 12], two players alternately claim unoccupied elements of the board of the game. The goal of a player is to claim a set of elements that form a winning set, and/or to prevent the other player from doing so. Tic-Tac-Toe, and its competitive variant played on a $15\times 15$ board, Gomoku, as well as Hex are the most well-known positional games. When the size of the board is not fixed, the decision problem, whether the first player has a winning strategy from a given position in the game is PSPACE-complete for many such games. The first result was established for Generalized Hex, a variant played on an arbitrary graph [8]. Reisch [24] soon followed up with results for gomoku [24] and Hex played on a board [25].

Recent work on the classical and parameterized computational complexity of positional games provides us with elegant first-order logic formulations of such domains [3, 4]. We draw inspiration from this approach and introduce a practical implementation for such games into QBF. We believe that Positional Games exhibit a class of games large enough to include diverse and interesting games and benchmarks, yet allow for a specific encoding exploiting structural properties.

Our contributions are as follows: (1) Introduce the Corrective Encoding: a generic translation of positional games into QBF; (2) We identify a few positional games of historical significance and put them forward to the QBF community as milestones of increasing difficulty; (3) Demonstrate on previously published benchmark instances that our encoding leads to more compact instances that can be solved faster by state-of-the-art QBF solvers; (4) Establish that the Corrective Encoding enables QBF solving of realistic small scale puzzles of interest to human players.

After a formal introduction to QBF and to positional games (Sect. 2), we describe the contributed translation of positional games into QBFs (Sect. 3). We then describe the selected benchmark game problems, including the proposed milestones (Sect. 4), before experimentally evaluating the quality of our encoding and comparing it to previous work (Sect. 5). We conclude with a discussion contrasting our encoding with related work (Sect. 6).

2 Preliminaries on QBF and Positional Games

We assume a finite set of propositional variables X. A literal is a variable x or its negation $\lnot x$. A clause is a disjunction of literals. A Conjunctive Normal Form (CNF) formula is a conjunction of clauses. An assignment of the variables is a mapping $\tau :X\rightarrow \{\bot ,\top \}$. A literal x (resp. $\lnot x$) is satisfied by the assignment $\tau$ if $\tau (x)=\top$ (resp. $\tau (x)=\bot$). A clause is satisfied by $\tau$ if at least one of the literals is satisfied. A CNF formula is satisfied if all the clauses are satisfied.

A QBF formula (in Prenex-CNF) is a sequence of alternating blocks of existential ($\exists$) and universal ($\forall$) quantifiers over the propositional variables followed by a CNF formula. A QBF formula may be interpreted as a game where an $\exists$ and $\forall$ player take turns building a variable assignment $\tau$ selecting the variables in the order of the quantifier prefix. The objective of $\exists$ (resp. $\forall$) is that $\tau$ satisfies (resp. falsifies) the formula.

Positional games are played by two players on a hypergraph $G=(V,E)$. The vertex set V indicates the set of available positions, while the each hyperedge $e\in E$ denotes a winning configuration. For some games, the hyperedges are implicitly defined, instead of being explicitly part of the input. The two players alternatively claim unclaimed vertices of V until either all elements are claimed or one player wins. A position in a positional game is an allocation of vertices to the players who have already claimed these vertices. The empty position is the position where no vertex is allocated to a player. The notion of winning depends on the game type. In a Maker-Maker game, the first player to claim all vertices of some hyperedge $e \in E$ wins. In a Maker-Breaker game, the first player (Maker) wins if she claims all vertices of some hyperedge $e\in E$. If the game ends and player 1 has not won, then the second player (Breaker) wins. The class of (p, q)-positional games is defined similarly to that of positional games, except that on the first move, Player 1 claims q vertices and then each move after the first, a player claims p vertices instead of 1. A winning strategy for player 1 is a move for player 1 such that for all moves of player 2 there exists a move of player 1...such that player 1 wins.

To illustrate these concepts, Fig. 1 displays a position from a well-known Maker-Maker game, Tic-Tac-Toe, and a position from a Maker-Breaker game, Hex. Although the rules of Hex are typically stated as Player 1 trying to create a path from top left to bottom right and Player 2 trying to connect the top right to bottom left, the objective of Player 2 is equivalent to preventing Player 1 from connecting their edges [20]. Therefore, Hex can indeed be seen as a Maker-Breaker positional game.

Fig. 1.

Two positional games played on the same vertices: a–i where vertex a has been claimed by Player 2 and vertices e and i have been claimed by Player 1.

3 The Corrective Encoding

In this section we present the Corrective encoding (COR). First we define positional games formally, describe the set of variables and the clauses in detail and analyse the size of the encoding.

3.1 Description

A positional game is a tuple $\prod = \langle T_\textsc {B} , T_\textsc {W} , \mathsf {F}, \mathsf {N}, E_\textsc {B} , E_\textsc {W} \rangle$ consisting of:

• Disjoint sets $T_\textsc {B}$ and $T_\textsc {W}$ of time points in which Black and White make moves. We denote $T=T_\textsc {B} \cup T_\textsc {W}$ as the set of all time points that range from $\{1,2, \ldots \mathsf {F}\}$. For example, in a positional game where black starts and $p=q=1$, $T_\textsc {B}$ contains all odd and $T_\textsc {W}$ all even numbers of T.

• $\mathsf {F}\in \mathbb {N}$ the depth (or length) of the game.

• A set of vertices $V=\{1 \ldots \mathsf {N}\}$ and two sets of hyperedges $E_\textsc {B}$ and $E_\textsc {W}$ of winning configurations for Black and White, respectively.

The remainder of this section defines a translation of a positional game configuration $\prod$ into a prenex QBF in CNF. For this we introduce variables defined in the following table. For readability we use a function style notation instead of variable subscripts. Let A denote the set of the two players $\{\textsc {B} ,\textsc {W} \}$.

Variable	Description
$\mathsf {time}(t)$	The game is still running by time point $t \in T$
${\mathsf {board}}(a,v,t)$	Player $a \in A$ owns vertex $v \in V$ at time point $t \in T$
$\mathsf {occupied}(v,t)$	Vertex $v \in V$ is occupied at $t \in T$
$\mathsf {win}(e)$	Black has claimed winning configuration $e\in E_\textsc {B}$
$\mathsf {move}(v,t)$	Vertex $v \in V$ is chosen at $t \in T_a$ by player $a\in A$
$\mathsf {moveL}(i,t)$	The moves for White encoded logarithmically, $0 \le i < \lceil \log _2(\mathsf {N}) \rceil \}$, $t\!\in \!T_\textsc {W}$
$\mathsf {ladder}(i,t)$	Auxiliary variables for the ladder encoding, $i\in V$ and $t\in T$

The last two sets of variables are of technical nature; $\mathsf {ladder}$ is used to encode that a player must claim 1 vertex when it is their time t to move, whereas $\mathsf {moveL}$ encodes the choices of White in a way that prevents the universal player from falsifying the formula by breaking the rules of the game.

Quantification. Here we specify the quantifier prefix of our encoding. In the order of the time point $t = \{1 \ldots F\}$ we introduce a level of quantifier blocks as follows:

(1)

On the innermost level we have

(2)

In the remainder of this section we list the clauses that make the body of the generated QBF instance. This body is constituted of sets of clauses encoding different aspects of the game. The encoding is almost entirely symmetric for both players apart from clauses which specify the interaction of the universal variables.

Time Handling. Variable $\mathsf {time}(t)$ holds if the game is not over at time point t.

(3)

Structure of the Board. Clauses (5) encode that both players cannot own the same vertex. One fundamental property of positional games is that claimed vertices never change owner. This basic property is captured in clause (6). Note that these two clauses are independent from the $\mathsf {time}$ variable and act also when the game is over. Once a vertex is claimed and ${\mathsf {board}}(a,v,t)$ is true the implication chain in (6) sets all board variables for that vertex in the future, in particular the last one ${\mathsf {board}}(a,v,\mathsf {F})$. Once the game is over (i.e. $\mathsf {time}(t)$ is set to false), then all unclaimed vertices stay unclaimed (7) and the situation of the board at the last active move of the game is propagated through to the final time point.

(4)

(5)

(6)

(7)

The following clauses (8)–(10) define the meaning of $\mathsf {occupied}$. Initially all vertices are unoccupied (8) and by definition a vertex is occupied if it is owned by Black or White.

(8)

(9)

(10)

Player’s Actions. The action clauses specify how the moves of the players affect the board. If player a claims vertex v at time $t\in T_a$, i.e. $\mathsf {move}(v,t)$ is true, then the game still has to be running (11). This clause can also be understood as if the game is over no moves are allowed anymore. Moreover, when $\mathsf {move}(v,t)$ is true, then vertex v was not occupied at the previous time point (12) and as a result of the action the vertex is occupied (13).

(11)

(12)

(13)

White’s Choice. The core of this encoding is how the universal variables interact with the rest of the encoding without having to prevent illegal moves by White. To avoid that White chooses too many vertices we encode the move logarithmically through variables $\mathsf {moveL}(i,t)$. Moreover, these variables only actually imply a move of White in case the game is still running and the vertex was unoccupied before. In case one of the prerequisites is not given, then no move will be forced by this clause. Let $L_1(v)$ denote to the set of indices that are 1 in the binary representation of v, likewise $L_0(v)$ where there is a 0. The following equality holds: $v = \sum _{j\in L_1(v)} 2^j$. For example, for $13=1101|_{2}$ the respective sets are $L_1(13)=\{0,2,3\}$ and $L_1(13)=\{1\}$.

(14)

Notice how these clauses interact with (11) and (12) such that any choice for the universal variables is not able to cause a contradiction. In case White chooses a combination of $\mathsf {moveL}$ that does not imply an existing vertex, then still a move is selected for White to satisfy the ladder encoding (see (21) to (25)).

Frame Axioms. The following two clauses specify what happens when no action is performed on a position and the board variable is unchanged. Clause (15) says that in time points where player s does not claim vertex v and the vertex has not been previously owned by s then it will also not be owned in the following step. In time points t of the opponent to s, all unclaimed vertices by s will be unclaimed in the next time point. Clause (16) forces this.

$$\begin{aligned} \{\mathsf {move}(v,t) \vee {\mathsf {board}}(a,v,t-1) \vee \lnot {\mathsf {board}}(a,v,t)&\mid a \in A, v \in V, t \in T_a \} \end{aligned}$$

(15)

$$\begin{aligned} \{{\mathsf {board}}(a,v,t-1) \vee \lnot {\mathsf {board}}(a,v,t)&\mid a \in A, v \in V, t \in T\setminus T_a \} \end{aligned}$$

(16)

Winning Configuration. For each winning configuration $e\in E_\textsc {B}$ we have introduced a variable $\mathsf {win}(e)$ and clauses (17) specifies that at least one of the winning configuration have to be reached and (17) defines which vertices belong to it.

White should never reach a winning position, for this we introduce a clause for each winning positions specified in clauses (19). We only need to encode this for the last time point F due to the implication chain (6). This looks straightforward from the definition, but we need to make sure with other clauses that White is unable to play illegal moves to reach a winning position.

(17)

(18)

(19)

(20)

Number of Moves. To restrict the number of moves we apply the ladder encoding  [9] to translate the cardinality constraint specifying the number of moves that a player can make in a round.

The ladder essentially encodes the equivalence $\mathsf {move}(i+1,t) \Leftrightarrow \lnot \mathsf {ladder}(i,t) \wedge \mathsf {ladder}(i+1,t)$. As soon as a move variable is set to true, all following ladder variables are forced to true (21, 22) and all previous are forced to false (21, 23). This ensures that no two move variables can be set to true. Clauses (25, 26) ensure that at least one move variable is true.

$$\begin{aligned} \{\lnot \mathsf {ladder}(i,t) \vee \mathsf {ladder}(i+1,t)&\mid i \in V, i < \mathsf {N}, t \in T \} \end{aligned}$$

(21)

$$\begin{aligned} \{\lnot \mathsf {move}(i,t) \vee \mathsf {ladder}(i,t)&\mid i \in V , t \in T \} \end{aligned}$$

(22)

$$\begin{aligned} \{\lnot \mathsf {move}(i+1,t) \vee \lnot \mathsf {ladder}(i,t)&\mid i \in V, i < \mathsf {N}, t \in T \} \end{aligned}$$

(23)

$$\begin{aligned} \{\mathsf {move}(1,t) \vee \lnot \mathsf {ladder}(1,t)&\mid t \in T \} \end{aligned}$$

(24)

$$\begin{aligned} \{\mathsf {move}(i+1,t) \vee \mathsf {ladder}(i,t) \vee \lnot \mathsf {ladder}(i+1,t)&\mid i \in V, i < \mathsf {N}, t \in T \} \end{aligned}$$

(25)

$$\begin{aligned} \{\lnot \mathsf {time}(t) \vee \mathsf {ladder}(\mathsf {N},t)&\mid t \in T \} \end{aligned}$$

(26)

These clauses also enforce a move by White even if White had chosen an already claimed vertex or no vertex with the $\mathsf {moveL}$ variables and clause (14) does not fire. This is a crucial property of the encoding. An arbitrary vertex for White is chosen by, the game continues and there is no backtracking even though the universal player acted illegal.

Initial Positions. The QBF generator can also translate positional games that contain initial positions of White and Black, i.e. vertices that players own before the actual game starts. It is straight forward to turn this into an equivalent description without initial positions: For each initial position v of one player remove this vertex from all its winning configurations and remove all winning configurations of the opposing player that contain v. After this operation we can remove v from V and have an equivalent game.

Symmetry Breaking. We employ a simple form of manual symmetry breaking by restricting the set of vertices from which the first move can be chosen. For instance in Generalized Tic-tac-toe (GTTT) and a $n\times n$ board, if this set contains the upper left triangle of the board (the set of coordinates (i, j) such that $1 \le i \le j \le n/2$), the symmetries of the squared board are broken. Typically, for other games with some initial positions for White and Black there is not much need for symmetry breaking since row or column symmetries are usually already broken by such a position.

Consecutive Moves. The positional game description need not have Black and White alternate moves: a description may allow a player to select several vertices consecutively. For instance, when $q=2$ players claim two vertices in each round. For the sake of simplicity, our presentation of COR above does not break this symmetry. Our implementation avoids such symmetries by merging consecutive moves into a single turn where a subset of vertices of the right cardinality must be chosen. We implemented this cardinality constraint as a sequential counter [26]. In coincides with the ladder encodings in the single move case.

3.2 Size of the COR Encoding

It is straightforward to estimate the number of variables and clauses of the encoding. For instance, clauses with a description containing $v\in V, t\in T$ are generated at most $\mathsf {N}\cdot \mathsf {F}$ times. Since the depth of a game is limited by the number of vertices, the number of clauses is roughly $20 \mathsf {N}^2 + \mathsf {N}\cdot |E_\textsc {B} | + |E_\textsc {W} |$.

4 Instances

We used the encoding above to generate three sets of QBF instances based on some well-known positional games.¹ The first two sets consist of positions of Hex and of a generalization of Tic-Tac-Toe on boards that are relatively small by human playing standards. Positions from that benchmark are fairly easy to solve even for relatively inexperienced human players of these games, and they can be solved almost instantaneously by specialized solvers. Our encoding of these positions should provide a reasonable challenge for QBF solvers as of 2019.

The third set contains the starting position of 4 positional games that are of interest to experienced human players and to mathematicians. At least 3 of these positions can be solved by specialized game algorithms developed in the 1990s and 2000s albeit with a non-trivial programming effort. The instances in this third set are out of reach of current QBF solvers and we believe that solving these positions with a QBF solver—via our encoding or a better one—can constitute a good milestone for the field.

4.1 Harary’s Tic-Tac-Toe and GTTT(p, q)

Harary’s Tic-Tac-Toe is a Maker-Maker generalization of Tic-Tac-Toe where instead of marking 3 aligned stones, the players are trying to mark a set of cells congruent to a given polyomino. This type of game has received accrued interest from the mathematical community which was able to show the existence of a winning strategy or lack thereof for most polyomino shapes. GTTT(p, q) is a further generalization of Harary’s Tic-Tac-Toe along the principle of (p, q)-positional games [7].

Previous work has already proposed an encoding of GTTT(p, q) played on small boards to QBF [7]. We refer to this existing in encoding as DYS. In our first set of benchmark, we encode the exact same GTTT(p, q) configurations as previous work. However, since our encoding is different, with obtain a different set of QBF instances. This provides us with an opportunity to directly compare our approach with existing work. We report results on the 96 instances of GTTT(1, 1) played on a $4\times 4$ board and compare formula size and solving performance with the DYS encoding.²

4.2 Hex

We use 20 hand-crafted Hex puzzles of board size $4 \times 4$ up to $7\times 7$ that all have a winning strategy for Player 1. The first 19 of these Hex instances are of historical significance. Indeed, they were created by Piet Hein, one of the inventors of Hex and first appeared in the Danish newspaper Politken [14, 20] during World War II [13].³ The remaining puzzle is a $5 \times 5$ position proposed by Cameron Browne, it arose during standard play and offers a significant challenge for the Monte Carlo Tree Search (MCTS) algorithm and the associated RAVE enhancement [5]. This is noteworthy because MCTS is the foundational algorithm behind the top artificial players for numerous games including Hex and Go [6].

4.3 Challenges

We now put foward a few positional games that have attracted the attention of board game players as well as AI or mathematics researchers. Table 1 summarizes the proposed challenges together with the size of their COR encoding.

Qubic, also known as 3-dimensional Tic-Tac-Toe, is played on a $4 \times 4 \times 4$ cube and the goal is to mark 4 aligned cells, horizontally, vertically, or diagonally. Our first domain was solved for the first time in 1980 by combining depth-first search with expert domain knowledge [21]. A second time in the 1990s using Proof Number Search (PNS), a tree search algorithm for two-player games [27].

The second domain, freestyle Gomoku, is played on a $15\times 15$ board and the goal is to mark 5 aligned cells, horizontally, vertically, or diagonally. Already in the 1930s, Gomoku was perceived to be giving an overwhelming advantage to Black [27], the starting player, and by the 1980s professional Gomoku players from Japan had claimed that the initial position admitted a Black winning strategy [1]. This was confirmed in 1993 using the PNS algorithm, a domain heuristic used to dramatically reduce the branching factor, and a database decomposing the work in independent subtasks [1].

Connect6 is akin to Gomoku but the board is $19\times 19$, the goal is 6 aligned cells, and players place 2 stones per move [16]. The Mickey Mouse setup once was among the most popular openings of Connect6 until it was solved in 2010 [30]. The resolution of Connect6 was based on PNS distributed over a cluster.

Our last challenge is an open-problem in Harary’s Tic-Tac-Toe which corresponds to achieving shape

on a $9 \times 9$ board. This problem was recently put forward as an intriguing challenge for QBF solvers [7] and we offer here an alternative, more compact, encoding.

Table 1. Selected problems put forward to the QBF community and size of their Corrective encoding. No preprocessing has been applied to these instances.

5 Analysis

5.1 Setup of Experiments

When solving problems encoded in QBF, the ideas underlying the encoding of a problem are only a factor in whether the instances can be solved withing reasonable resources. Two other important factors are the specific solver invoked and the kind of preprocessing performed on the instance before solving, if any. In our experiments, we chose four state-of-the-art QBF solvers, including the top three solvers of the latest QBF Competition⁴ and three preprocessors, as indicated in Table 2a.⁵ All software was called with default command line parameters.

Table 2. Software used and resulting performance on the first benchmark.

The experiments have been running on a i7-7820X CPU @ 3.60 GHz with 8 cores, 24 GB RAM. All solvers have been running with a dedicated single core.

5.2 Experimental Comparison of Our New Encoding to the DYS

Before attempting to solve positional games, let us first examine how large and amenable to preprocessing the generated encodings are. We use an approach inspired by recent work on QBF preprocessors [19] and report in Table 3 the number of quantifier blocks, universal and existential variables, clauses, and literals, as well the time time needed for the preprocessing of a representative instance of GTTT(1, 1). On both the existing DYS encoding and our proposed COR, we test each preprocessor individually as well as the outcome of running one preprocessor then another. No preprocessor timed out.

Table 3. Preprocessing on $5\times 5$ instance gttt_1_1_00101121_5x5_b

Two observations stand out when looking at Table 3. First, DYS is much larger than COR across most of the size dimensions. Second, preprocessors seem to be much more capable or reducing the size of the DYS instance than the size of the COR instance. Our interpretation is that it is a direct consequence of the effort we have put in crafting the proposed new encoding: there is relatively little improvement room left for the preprocessors to improve the formulas. Since the size of a formula directly impacts how hard it is to solve, we expect QBF solvers to struggle much more with DYS-encoded game instances than with COR-encoded ones.

In our next experiment, we compare how well QBF solvers manage to solve GTTT game instances when encoded with DYS and with COR. Since different preprocessors tend to play to the strength of different solvers, we report the preprocessor that lead to the best performance for each solver separately. We compare the solvers and the encodings using 96 GTTT(1, 1) $4\times 4$ game instances and assuming a timeout of 1000 s, Table 2b displays for each configuration the number of formulas solved (S), proven satisfiable ($\top$), proven unsatisfiable ($\bot$), and unsolved (U), as well as the cumulative time spent by the solver.

The data in Table 2b confirms our intuition. GTTT games can be more effectively solved through our encoding: 3 out of 4 solvers solve all COR instances whereas none solve all DYS instances, and COR instances are solved between up to two orders of magnitude faster. Furthermore, our results demonstrate that the choice of encoding has a bigger impact than the choice of solver and preprocessor.

5.3 Solving Increasingly Realistic Games

Iterative deepening is an algorithmic principle in game search recommending to search for a d-move strategy before attempting to find a deeper one. This principle lets one benefit from the memory-efficiency of depth-first search and from the completeness of breadth-first search. It is easily adapted to solving games via QBF: encode one formula per depth and attempt to solve them one by one in order. We demonstrate the benefits of this adaptation in Fig. 2: the position admits a depth 5 winning strategy. Proving the existence of a strategy of depth $\le$5 needs 0.1 s, but the formula stating the existence of a strategy of depth $\le$13 needs 2 hours to be proven. Although the outcome of searches at short depths is subsumed by that of deeper searches, the exponential growth of the required solving time makes iterative deepening a worthy trade-off.

Fig. 2.

GTTT $5\times 5$ L game where Black can force a 5-move win.

Our final benchmark is the set of 20 historical Hex puzzles described in Sect. 4.2. Except for one puzzle on which qesto needed more than 10 GB of memory, all positions on board sizes $5\times 5$ or less can be solved by state of the art QBF solvers (Table 4). The 5 remaining puzzles remain out of reach at this stage. This is a remarkable feat: for the first time, the QBF technology can address game situations considered of interest to human players.

Table 4. Solving classic Hex puzzles by encoding them through COR.

6 Comparison to Related Encodings

Despite the similarity of QBF solving with systematic search for winning strategies in games with perfect information, to the best of our knowledge there are not many encodings published that have attempted translation from games to QBF. After Walsh [28] challenged the QBF community to solve Connect4 on a $7\times 6$ board using QBF techniques in 2003, there was some activity in this direction but with rather little success in experiments.

The first concrete and implemented encoding of a game is the work by Gent and Rowley that presents a translation from Connect4 to QBF [11]. Building upon Gent’s encoding [2] presents a QBF encoding of an Evader/Pursuer game that resembles simpler chess-like endgames on boards of size $4\times 4$ and $8\times 8$. Both papers analyse problems that are not positional games, but the authors do report similar challenges in the construction of QBF formulas.

The closest to our encoding is the DYS encoding of GTTT [7] that has been proposed recently which is an adaptation of the encoding for [11]. The structure and clauses for these two encodings are similar so our more detailed comparison to DYS also applies to the encoding in [11].

Apart from these games and encodings to the best of our knowledge we are not aware of any other QBF formulations of games that improve upon them. In the remainder of this section we will go into various properties regarding COR and the existing encodings.

Generalisation. Although we presume that the ideas behind DYS could be extended to arbitrary positional games, the description of the encoding was tailored to the GTTT domain. We chose positional game as an input formalism to reach a reasonable level of generalisation, i.e. many two-player can be formulated as positional games, but enough structural properties from the description to create neat encodings.

Clausal Description. The description of the clauses in DYS is not purely clausal and contains many equivalences. The general translation of equivalences into CNF introduces auxiliary (Tseytin) variables of which some can be avoided through better techniques. Our description consists only of clauses and much work has gone to reduce the number of variables.

Size. The size of our encoding is quadratic in the number of vertices and linear in the number of winning configurations. Even for smaller boards these scale effects materialize and we demonstrate and discuss our observations in the following Section.

Binary Clauses. Binary clauses enjoy many theoretical and practical advantages. A purely 2CNF problem can be solved in polynomial time, SAT solvers invest in the special treatment of binary clauses to speed up propagation and learning. This should also apply to QBF solving. Discovering a binary clause structure of a certain aspect of a problem description might be the key to crafting encodings that also solve fast. Our encoding demonstrates that many aspects of positional games can be captured through sets of binary clauses forming chains.

Timing. The variable $gameover_z$ in DYS has the same meaning as $\mathsf {time}$ in our encoding, it marks the end of the game and is crucial to prevent white from reaching a winning position after black has already won. In DYS this variable is added to almost all clauses such that when the game is finished the universal variables cannot falsify these clauses anymore. This technique produces correct encodings, but affects propagation negatively and weakens clause learning. We avoid such weakening of the other clauses by de-coupling time and the board structure of a game. When the game is finished (i.e. $\mathsf {time}$ is set to false) independently of the choices of the players no moves are allowed anymore and all empty board positions are propagated through to the end. We expect that COR makes it easier for the solver to exploit transposition of sequence of moves leading to the same board configuration than previous encodings.

Monotonicity. Using the property of monotonicity of positional games—the set of claimed vertices only grows throughout the game—our clauses manage to captures this property more directly than the previous encodings. For instance, DYS introduces variables that are true if a player wins in time point t by reaching a winning configuration. We avoid the need to know explicitly by which time point a player won via propagating the claimed vertices through to the last time point and only need to test for the winning configuration of both players there. Through de-coupling the time aspect of games from checking winning positions our encoding has fewer variables and shorter clauses, that again benefit propagation.

Adapted Log Encoding. This concept was first introduced for the encoding of quantified constraint satisfaction problems (CSPs) into QBF [10]. There, a logarithmic number of universal variables encode the binary representation of a CSP variable. This technique was also applied with success in a game encoding to QBF [2].

Indicator Variables. To the best of our knowledge all translations of games (including non-positional ones) to QBF introduce variables that indicate types of illegal moves by white. Such variables again weaken the encoding due to longer clauses. The encoding DYS has the following types of illegal moves; white claims too many vertices, too few vertices, already occupied vertices. All of these are explicitly encoded in DYS whereas COR corrects white’s move. The key insight in the work of [2] raises the question how to address White’s illegal behavior without weakening the encoding or introducing auxiliary variables.

7 Conclusion and Future Work

We consider the craft of finding efficient translations of a problem description to the clausal representation an important step towards better performances of QBF solvers. Our investigation regarding the class of positional games demonstrates that a carefully crafted translation using structural properties to decrease and shorten clauses and decrease the number of variables improves the applicability beyond trivial problems. We list some key insights:

• Binary implication chains capturing monotone structural properties of problem are crucial.

• Variables representing illegal moves by the universal player can be avoided.

• Encoding the choices of the choices by the universally player logarithmically helps in this problem description.

• Preprocessing is crucial for previous encodings to perform, whereas on our encoding has minor impact.

Our investigation focused on clause representation and we have yet to extend to non-clausal description languages to QBF such as QCIR.

The insights from our investigation can be applied to translation of other almost-positional games and to planning problems with similar structures.

Although Hex is a positional game, its hypergraph representation is exponential in the board size because it needs to account for all paths between a pair of sides. For larger boards one will need an implicit representation of the paths between the two sides, possibly drawing inspiration from existing first-order logic modeling [4].