This is the first of the problems in the “Games and Puzzles” section. The way they express these problems as logical formulas are pretty neat.
The problem: Generalized Hex. This is problem GP1 in the appendix.
The description: Given a graph G=(V,E) and two vertices s,t in V. Players alternate coloring vertices (except for s and t) “blue” (by player 1) and “red” (by player 2). Player 1 wins if a path of blue vertices from s to t ever exists, and player 2 wins if that becomes impossible. Does Player 1 have a forced win?
G&J mark this problem as “not known to be in NP” (like many of these problems), and the paper by Even and Tarjan mentions that it’s likely that this problem is even harder than NP-Complete problems, since we may not even be able to solve it in polynomial time with a non-deterministic algorithm.
Example: Here’s a picture of the “standard” Hex game that I took from the Internet:
The hexagonal spaces are the vertices of the graph. In the “standard” game, the vertices are only adjacent to their neighbors, but the generalized game allows for different kinds of connections. In the “standard” game of hex, you can connect from any hex on one blue edge of the board to any hex on the other blue edge- we can add that in the generalized game by making an edge from every cell on one blue edge to s, and another set of edges from every cell on the other side to t.
The other big difference is that in the standard game, either blue has a path connecting the 2 blue sides or red has a path connecting the 2 red sides (so blue not being able to create a path means red has a path). In the generalized game, there are no “red sides”, so all we care about is whether blue can create a path or not.
In the above image, blue does not have a win (because red has already won). But if we look at a slightly different board:
If the hex marked green is blue instead of red, then blue has a forced win, no matter whose turn it is. Either of the two cells next to the left blue edge will win the game for blue.
Reduction: As I alluded to last week, many of these problems reduce from QBF. So the question is: How do we take an arbitrary formula and turn it into a game board that has a forced win for player 1 if and only if the formula is solvable?
To help us, Even and Tarjan create some subgraphs that have properties that will help us. First is a tree where the root connects to s, and some leaves connect to t:
It turns out that if it’s blue’s turn, blue has a forced win if and only if all of the leaves connect directly to t: Your first move is the root (above s), and then each move after that you choose the child node that is the root of a subtree that red has not played in.
If there are leaves that are not connected to t, red can win by always picking a node in the subtree that is connected to t. In the graph above, if blue picks the root, red would pick the left child, forcing blue to move right. Then red picks the right child of blue’s node, and then the left child of blue’s next move.
(If blue doesn’t pick the root on their first move, or if blue doesn’t pick a child of their last move, red can disconnect the whole tree.)
The way to think of this graph is that it is similar to “and”.
Here’s another tree structure:
This graph has one child of the root connecting directly to t, and otherwise sets pairs of grandchildren that may or may not connect directly to t- all of the a’s connect to t, and the b’s may or may not connect to t. If it’s blue’s turn, they have a forced win if and only if there is at least one b vertex that connects to t. (Blue picks the root, red has to pick the child that connects directly to t, then blue picks the child that has both a and b connect to t, and red can’t stop it).
The way to think of this graph is “or”. (The caption in the figure in the paper says this represents a “conjunction” which I’m pretty sure is a typo).
The third graph is based on variables:
There are 2 copies of each variable and their negation. If it’s blue’s move, they can pick either x1(1) or x1(2) or their negations. Then red has to pick the negated vertex of the opposite number (if blue picks x1(1) then red has to pick ~x1(2)). This will be used to force a variable to only have one truth value. If it’s red’s move, they can decide whether to use the positive or negated version of x1 and blue’s moves are forced. So, if it’s blue’s move when this ladder is reached, it works like a “there exists”- blue can choose any combination of literals they want. If it’s red’s move, this works like a “for all”- red can force blue into whatever variable configuration that they want.
So we’re given a QBF formula. We’ll assume the expression part of the formula is in CNF. We create a graph that has s,t, 4 vertices for each variable (xi(1), xi(2), ~xi(1) and ~xi(2) for each variable xi). For each change in quantifier (between ∀ and ∃) we add a “quantifier” vertex qi . We can assume the first quantifier in the formula is a ∀, so the first quantifier vertex is placed in such a way that blue needs to play on it (effectively wasting its turn and giving red the initiative to select the first part of the next set of vertices). If the next quantifier is a ∃, we add the quantifier vertex such that blue will reclaim the initiative
For each clause, we add an “and” tree, where the “b” leaves of the tree connect to the corresponding literals of the clause.
Here is the paper’s example for a small formula:
Some things I noticed to help me understand what is happening:
- The formula starts with ∃, so blue can pick either x(1) or ~x(1).
- The formula then moves into a ∀, so blue will have to pick q1, meaning red gets to decide whether blue will pick y(1) or ~y(1)
- The formula then moves into a ∃, which means after blue’s choice, red has to pick q2, giving blue the choice about z(1) or ~z(1)
- The l vertices denote the subtrees. They are built out of the trees discussed earlier, and the paths through the “b” vertices (the one next to the “a” vertices) connect to the literals that are in each clause.
There are a lot more details about how it all gets exactly connected, but I think this shows the main idea of how the game is set up.
Difficulty: 8. This is a very cool transformation, but you need a lot of help to see the structures and forcing moves. On top of that, there are a lot of fiddly details that I’ve glossed over that are important in an actual reduction.