Solving Pips puzzles with MiniZinc
The New York Times released their latest online game, Pips, a little over a month ago. Continuing a theme of using way too much compute on NYT puzzles, I decided to learn how to use an SMT solver with the goal of automatically solving Pips puzzles. While doing preparatory research for this post, I found that Joe Kerrigan had already published a nice writeup of how to do this in Z3, so I figured that for novelty’s sake I should try out MiniZinc. For bonus novelty points, our approach to setting up the constraints is going to be dramatically different from, and perhaps slightly better than, the approach in that blog post.The anatomy of a Pips puzzle
A Pips puzzle consists of the following data:- a set of distinct dominoes, each of which has from zero to six pips on both of its component tiles;
- a board that can be tiled with dominoes;
- a set of disjoint regions , each with a constraint.
- all-equal: all tiles in the region have the same number of pips;
- none-equal: no two tiles in the region have the same number of pips; and
- less-than/equal-to/greater-than: the total number of pips on the tiles in the region is less than/equal to/greater than a prescribed number.
Alternatively, we could require that the regions cover but allow regions with trivially-true constraints.
, and puzzles don’t necessarily have unique solutions.
Prior art
The idea behind the approach in Joe Kerrigan’s post is to have two two-dimensional arrays of decision variablestile_id[r,c] and pip_count[r,c]. Each domino is treated as being composed of two tiles, with domino i corresponding to tiles 2*i and 2*i+1. It is relatively easy to write down constraints that ensure that tile 2*i has tile 2*i+1 as one of its neighbors, and that every tile appears exactly once. Further constraints ensure that the tile_id and pip_count arrays match up (i.e., that whatever value the tile ID at (r,c) prescribes is actually the value in pip_count[r,c]). Then the region constraints are straightforwards to write down in terms of pip_count.
Starting centers
The main idea behind our approach is to take advantage of the underlying checkerboard coloring of the board : we know that, writing we have and that every domino covers one point in and one point in . So we’ll arbitrarily call the points in the centers of the dominoes, and our solution will be described by three decision variables associated to each of then_dom centers:
domino_id(anint): which domino is covering this center?domino_dir(anenum): which direction (N/S/E/W) is the domino covering this center pointing?domino_flip(abool): is the domino covering this center flipped from how it appears in our list of dominoes? (In other words, if it’s given to us as[1,6], is the1covering the center or is the6?)
cell_pips (of size n_cell = 2*n_dom) corresponding to the pip values of all of the cells of the puzzle. This array is said to be derived because we can compute it from the three decision variables above using a system of constraints.
Supply constraints
Our remaining constraints then become quite natural:- the
domino_idsvalues must all be distinct; - the
domino_dirsvalues must all be valid (no domino can be pointing off the board); - the
domino_dirsvalues cannot cause two dominoes to overlap; and- This is ensured by means of passing a
dir_cell_indicesarray that indicates which indices incell_pipscorrespond to placing dominodin each of the four directions (or-1if that direction is not valid). Then we can just require that the values ofdir_cell_indices[domino_dir[i]]are all distinct.
- This is ensured by means of passing a
- the region constraints must all be satisfied.
- This is ensured by encoding each region as an array of indices into
cell_pipsand then constraining the appropriatecell_pipsvalues.
- This is ensured by encoding each region as an array of indices into
domino_flip booleans for dominoes that have the same number of pips on both tiles. Note that the constraints on sums are the only constraints that make an SMT solver more appropriate than a SAT solver.
Obstruction theory
(Disclaimer: I am very unfamiliar with SAT/SMT solvers; the heuristics in this section may all be totally wrong.) One worrying aspect of both approaches is that there are “non-local” constraints on thetile_id/domino_dir variables. To see this, suppose that we have a configuration like the following:
tile_id value of the darkened square, then using the sibling value for the square above or (in our approach, further supposing that the darkened square is a center) guessing the domino_id value of the darkened square and guessing its domino_dir value to be NORTH. What will happen under these circumstances? It is possible that the solver is able to make quite a bit of progress finding partial solutions to the remainder of the puzzle, and spends quite a lot of time doing so. (This seems like it would be even more of a problem for Pips puzzles with large numbers of solutions; most hard Pips puzzles have a small number of solutions.) But all this effort is in vain, for the initial choice has created a disconnected region that is obviously not tileable by dominoes.
It’s not clear how significant of a problem this is, or how to address it if it is in fact a significant problem. Perhaps some heuristics on which variables to guess first would help?
The thief of joy
I went ahead and reimplemented Joe Kerrigan’s grid-based approach in MiniZinc in order to compare performance against our center-based approach, then ran the two models on my laptop against all of the hard puzzles from August 18 through September 28.
Try it yourself!
The code is up on my GitHub.Digestif: a very confusing bug
I ran into a couple of bugs while coding this up (helped very much by Claude Code during both coding and debugging). The first was a relatively straightforward bug to hunt down: in the less-than/greater-than regions, Claude had interpreted the constraints as “every tile must have more/fewer than the target number of pips”. (The official rules are very clear on this distinction.) This faulty code generation was probably exacerbated by poor initial naming choices for the region types on my part. Thankfully, this bug was easy to track down, since several puzzles became unsatisfiable and a straightforward trace of failing clauses showed the error. The second bug was a real doozy, however. I wanted to use lighter separators for the internal edges of dominoes so that it was obvious which way they were oriented. The current code uses ╪ (for horizontally-oriented dominoes) and ╫ (for vertically-oriented ones), but my original choice was : and ܅ (U+0705, a horizontal colon) to achieve a sort of dotted-line effect in terminal. My code had some bizarre output corruption where certain separator/junction characters were in the wrong spots, as in the image below:
- Displaying just the pip counts looked fine.
- Displaying only the “junction” characters at the corners of dominoes looked fine.
- The underlying boolean arrays for whether we should include horizontal and vertical separators looked fine.
- Displaying just the vertical separators looked fine.