There’s a lovely new puzzle game for the iPhone called Adrift. I got it last week when I was in bed with flu, and it’s a fun way to spend a few hours.
The puzzles look like this:
And you solve them by connecting the coloured stars with paths of the same colour:
You can play a few demo levels on the web. This is a very simple example. Some of the more difficult ones are pretty fiendish.
But this post isn’t about how to solve Adrift puzzles. It’s about their computational complexity. (I seem to be making a habit of investigating the complexity of puzzle games once I’ve finished playing them.) Intuitively it seems pretty likely that Adrift puzzles are NP-complete, because they are difficult enough to be satisfying but it’s easy to verify that a solution is correct.
Recently I read Games, Puzzles & Computation, which introduces an elegant general “Constraint Logic” framework for proving complexity results about games, and Adrift seemed like a good excuse to try out these techniques.
The basic technique for proving hardness results is reduction. We want to show that, if there were a fast algorithm for solving Adrift puzzles, it could be used to solve some problem that is known to be NP-hard. The most promising-looking such problem from Games, Puzzles & Computation is Constraint Graph Satisfiability (§5.1.3). So we need to invent a translation that will convert any Constraint Graph Satisfiability problem into an Adrift puzzle.
A constraint graph is a finite planar graph with red and blue edges, and three edges meeting at each node. Like this:
We can also suppose that every node joins either three blue edges (making it an OR node) or else two red and a blue (an AND node).
To solve a Constraint Graph Satisfiability problem, you draw an arrow on each edge of the graph so that every node has either at least one blue arrow pointing at it, or at least two red ones. In the picture the blue edges are drawn twice as thick as the red ones, to illustrate the fact that two reds are worth the same as one blue.
Why not try to solve this? It’s not difficult, but it’s possible to get stuck if you make the wrong choices early on.
In fact, there is more than one solution. Here is one:
Now we’re going to show that, if Adrift puzzles are easy, then so is Constraint Graph Satisfiability. If you give me a CGS problem, I’ll convert it into an Adrift puzzle as follows. Suppose the constraint graph is drawn on a grid, and replace each cell of this grid by a 5×5 square section of an Adrift puzzle, according to the following rules:
- An OR node turns into this gadget, using two previously unused colours:
- An AND node turns into this gadget:
where one of the three entrances is connected to the central island, corresponding to the blue edge in the constraint graph. So there are three possibilities, depending which edge is blue:
- Finally, an edge is represented like this – again using a colour that hasn’t been used elsewhere. These wires can be arbitrarily long, and go round corners. There is only one pair of colours for each wire, however long and bendy it is.
And really that is the end of it, though I still need to persuade you that these gadgets work as advertised.
Each wire can either be resolved this way
or this way
corresponding to the two directions of the arrow in the satisfied constraint graph. My mnemonic for the direction of the arrows is to imagine the coloured band as a catapult or a bow, propelling the arrow in the given direction.
Here is a fully-loaded OR gadget with three inputs attached:
and here is one possible resolution of the gadget:
It should be clear that this really does function as an OR: you can’t have all three arrows pointing away from the node, because there isn’t room for all three colours in the middle.
Likewise the AND gadget looks like this when hooked up to three wires:
and one possible resolution is like this:
Again it should be fairly clear that this functions as advertised: you can’t have the blue and one of the red arrows pointing away from the node, because there isn’t room.
So that’s it. One more entry in the long list of NP-complete puzzle games. If you’re interested in this sort of thing, I recommend Games, Puzzles & Computation. It’s full of interesting results and tantalising open problems. The constraint logic technique is especially useful for PSPACE-hard puzzles like Sokoban.
Update on 14 March: There is nothing new under the sun. It turns out this theorem was proved in 1975 by James F. Lynch at the University of Colorado, by direct reduction from CNF-SAT: The equivalence of theorem proving and the interconnection problem. Thanks to reddit commenters for pointing me in the right direction to find this.