Solving the GCHQ Christmas puzzle (part 1) with Constraint Programming

The GCHQ Christmas card puzzle has had us all scratching our heads at Forgerock Engineering in Bristol this week (well, that and trying to get OpenAM 13 ready, on which more to come soon). Some colleagues have solved the first part by hand. As a lazy programmer though, this seems like such a waste of energy. What if I ever want to solve another such puzzle?!  So I decided to solve the puzzle automatically, and constraint programming seemed like the obvious approach as the puzzle is effectively a set of constraints over the shading of a grid. Warning: spoilers ahead if you’ve not solved the first stage already.

Initially, I wrote my own specialised constraint solver using Java 8 and two BitSets to represent the possibility of each square being white or black. This worked well enough, and the solution was found very quickly (~200ms without JIT warmup) once debugged. However, I’d like to now show you the same solution written using the Choco Constraint Programming library, as it really is quite a nice solution and a much more general framework. The full source code of the solution is here.

The first step is to create a Solver and define the variables that will make up the solution. As the nonogram is defined as a 25×25 grid, and each square can either be white or black, it makes sense to define the puzzle as a matrix of boolean variables:

private static final int GRID_SIZE = 25;
...
final Solver solver = new Solver("GCHQ Christmas Nonogram");
final BoolVar[][] grid = VariableFactory.boolMatrix("grid", GRID_SIZE, GRID_SIZE, solver);

This defines a 25×25 array of boolean constraint variables. Each variable can be instantiated to either true (1) or false (0), or it can be undetermined if the solver hasn’t discovered its value yet. The variable at grid[x][y] represents the value of the cell at column x (counting down from the top) and row y (left-to-right): a 0/false means that the cell should be white, while a 1/true means it should be black.

The first step is then to define the fixed black cells defined for the puzzle. We do this by adding constraints (using a constraint on the underlying SAT-solver) that these cells must be true:

public static final int[][] KNOWN_POSITIONS = new int[][] {
 {3, 3}, {4, 3}, {12, 3}, {13, 3}, {21, 3},
 {6, 8}, {7, 8}, {10, 8}, {14, 8}, {15, 8}, {18, 8},
 {6, 16}, {11, 16}, {16, 16}, {20, 16},
 {3, 21}, {4, 21}, {9, 21}, {10, 21}, {15, 21}, {20, 21}, {21, 21}
 };
...
for (int[] coords : KNOWN_POSITIONS) {
    SatFactory.addTrue(grid[coords[0]][coords[1]]);
}

We can then think about how to formulate the actual puzzle constraints. When I was discussing this with a colleague, I initially toyed with the idea of using regular expressions to test whether a given constraint had been satisfied. The idea was that to test a constraint like “7 1 3”, you could use a regular expression of the form (using ‘#’ to represent blocks and spaces for spaces) “\s*#{7}\s+#\s+#{3}\s*” – that is, zero or more spaces, followed by exactly 7 blocks, then 1 or more spaces (because there must be at least one space between each run of blocks), followed by 1 block, etc.

It turns out that Choco has a FiniteAutomaton that allows us to do exactly this! Instead of using spaces and # characters, we use 0s and 1s. Given an array of run-lengths, generating the regular expression can be done quite easily with Java 8 streams:

 private static String regularExpression(int[] runLengths) {
     return "0*"
         + Arrays.stream(runLengths)
                 .mapToObj(x -> String.format("1{%d}", x))
                 .collect(Collectors.joining( "0+"))
         + "0*";
 }

This converts the array of run lengths into a Stream, and converts each into a regular expression of the form “1{n}” where n is the run length. We then join consecutive run-lengths with 1 or more spaces (0+), and finally surround the whole thing in 0* expressions to allow any amount of space at the ends of the row/column.

Given this, we can then easily define all the constraints for the rows and columns as defined in the puzzle:

public static final int[][] COLUMN_CONSTRAINTS = new int[][] {
     {7, 2, 1, 1, 7},
     {1, 1, 2, 2, 1, 1},
     {1, 3, 1, 3, 1, 3, 1, 3, 1},
     ...
...
for (int col = 0; col < Grid.COLUMN_CONSTRAINTS.length; ++col) {
    String re = regularExpression(Grid.COLUMN_CONSTRAINTS[col]);
    solver.post(IntConstraintFactory.regular(grid[col], 
        new FiniteAutomaton(re)));
}

We can do the same for the row constraints, with the only difference that we need to first copy the variables representing the row out of the grid because they are not contiguous:

for (int row = 0; row < Grid.ROW_CONSTRAINTS.length; ++row) {
    String re = regularExpression(Grid.ROW_CONSTRAINTS[row]);
    BoolVar[] rowVars = new BoolVar[GRID_SIZE];
    for (int x = 0; x < GRID_SIZE; ++x) {
        rowVars[x] = grid[x][row];
    }
    solver.post(IntConstraintFactory.regular(rowVars, 
        new FiniteAutomaton(re)));
}

All that remains is then to ask the solver to solve the constraints and to write out the result as an image:

if (solver.findSolution()) {
  Solution solution = solver.getSolutionRecorder().getLastSolution();
  final int scale = 10;
  BufferedImage image = new BufferedImage(scale * GRID_SIZE, scale * GRID_SIZE, BufferedImage.TYPE_INT_RGB);
  Graphics2D graphics = image.createGraphics();
  for (int y = 0; y < GRID_SIZE; ++y) {
    for (int x = 0; x < GRID_SIZE; ++x) {
      Color colour = solution.getIntVal(grid[x][y]) == 1 ? Color.BLACK : Color.WHITE;
      graphics.setColor(colour);
      graphics.fillRect(x*scale, y*scale, scale, scale);
    }
  }
  ImageIO.write(image, "PNG", new File("/tmp/solution.png"));
  Chatterbox.printShortStatistics(solver);
}

And then we just run it and get the result:

1 Solutions, Building time : 0.275s, Resolution time 0.030s, 3 Nodes (99.4 n/s), 0 Backtracks, 0 Fails, 0 Restarts

I hope you enjoyed this exploration of the power of constraint programming. If you love solving interesting problems, why not come and work with us at Forgerock? We’re an open-source company, and we’re hiring Java and UI developers, QA engineers, sales engineers, account managers and more across multiple locations in the UK, US and around the world.

Update 15th Jan 2016: It turns out that there is another working solution to this puzzle that I have discovered by accident. I was testing an improvement to the code to use Choco’s built-in matrix transposition utility function, but I made a mistake: I ended up transposing the row and column constraints while leaving the “fixed” squares from the initial problem in their original positions. To my surprise, this still yielded a solution, and even more surprising, when I scanned the resulting image it took me to the same page as the correct solution! The image appears to be the same as the original solution but a mirror image and rotated through 90 degrees. I suspect my QR scanner is just correcting these distortions (using the anchoring points and other features) to produce the correct solution.