Conway’s Quintomino

A quintomino is a pentagonal tile whose five edges are labelled with the numbers $1$ through $5$ in some cyclic order. Two quintominos are considered the same if one can be rotated or reflected to the other; under this equivalence there are $5!/(5 \cdot 2) = 12$ distinct quintominos. The twelve quintominos are the twelve bracelets of $\{1, 2, 3, 4, 5\}$. The coincidence with the dodecahedron’s twelve pentagonal faces is too beautiful to ignore, and Conway proposed the natural puzzle that follows: place all twelve quintominos on the twelve faces of a regular dodecahedron — each piece used once, in any rotation or reflection — so that every pair of abutting edges shows the same number.

The puzzle has $12!$ placements times $10^{12}$ orientations, a search space of roughly $5 \cdot 10^{20}$, but the edge-matching constraint is so tight that any feasibility question the solver is asked is answered in hundreds of milliseconds. Conway’s original question (does the puzzle admit a solution?) is resolved in the affirmative.

Geometry of the dodecahedron

The regular dodecahedron has $12$ pentagonal faces, $30$ edges, and $20$ vertices. Each face is adjacent to five others, sharing one edge with each. A convenient encoding of the face-adjacency structure is to identify faces with the twelve vertices of the regular icosahedron (the dodecahedron’s dual). Using the standard vertex coordinates $$(0, \pm 1, \pm \varphi), \quad (\pm 1, \pm \varphi, 0), \quad (\pm \varphi, 0, \pm 1),$$ where $\varphi = (1 + \sqrt{5})/2$ is the golden ratio, two faces are adjacent exactly when the corresponding icosahedron vertices are at distance $2$. There are exactly $30$ such pairs, matching the $30$ edges of the dodecahedron.

For each face $f$, the five neighbours need to be listed in a definite cyclic order (anti-clockwise when viewed from outside the solid), giving a labelling $\mathrm{edge}(f, e)$ for $e \in \{0, 1, 2, 3, 4\}$. The edge-pairing is then an involution: if $\mathrm{edge}(f, e) = g$, then $\mathrm{edge}(g, e') = f$ for exactly one $e'$, and we call $\bigl((f, e), (g, e')\bigr)$ an edge-correspondence. There are $30$ such correspondences, one per physical edge of the dodecahedron.

The twelve bracelets

The twelve distinct quintominos are shown in Figure 9.1. A canonical representative is chosen by fixing the vertex labelled $1$ and listing the remaining labels anti-clockwise starting from it; the twelve pieces are then enumerated by the $4!/2 = 12$ equivalence classes of $\mathrm{Perm}\{2, 3, 4, 5\}$ under reversal.

The programming model

The encoding follows a now-familiar pattern: for each face choose a piece and an orientation; tie the five edge labels to those choices via a table constraint; enforce distinctness of pieces and equality across edge-correspondences.

Variables

For each face $f \in \{0, \ldots, 11\}$ let $\mathrm{Piece}_f \in \{0, \ldots, 11\}$ be the piece assigned to face $f$, and let $\mathrm{Edge}_{f, e} \in \{1, 2, 3, 4, 5\}$ be the number on face $f$’s edge $e$ for $e \in \{0, 1, 2, 3, 4\}$. The face’s orientation is implicit in the choice of edge tuple.

Piece-orientation table

Each quintomino $B$ admits ten distinct placements on a pentagonal face: five rotations times two reflections (since the labels are distinct the orbit has full size). Enumerate, for each piece, those ten $5$-tuples; for each face $f$ impose $$\bigl(\mathrm{Piece}_f, \mathrm{Edge}_{f, 0}, \ldots, \mathrm{Edge}_{f, 4}\bigr) \in \text{Placement table}.$$ The table has $12 \cdot 10 = 120$ entries.

Piece uniqueness

$$\operatorname{AllDifferent}(\mathrm{Piece}_0, \ldots, \mathrm{Piece}_{11}).$$

Edge-matching

For every edge-correspondence $\bigl((f, e), (g, e')\bigr)$, $$\mathrm{Edge}_{f, e} \;=\; \mathrm{Edge}_{g, e'}.$$ There are $30$ such constraints.

A solver in sixty lines

from ortools.sat.python import cp_model
from itertools import permutations
import math

PHI = (1 + math.sqrt(5)) / 2
ICO = [
    (0, 1, PHI), (0, -1, PHI),
    (0, 1, -PHI), (0, -1, -PHI),
    (1, PHI, 0), (-1, PHI, 0),
    (1, -PHI, 0), (-1, -PHI, 0),
    (PHI, 0, 1), (-PHI, 0, 1),
    (PHI, 0, -1), (-PHI, 0, -1),
]

def dot(u, v):
    return sum(a * b for a, b in zip(u, v))

def neighbours(V, eps=1e-6):
    N = [[] for _ in range(12)]
    for i in range(12):
        for j in range(12):
            if i == j: continue
            d = sum((V[i][k] - V[j][k]) ** 2
                    for k in range(3))
            if abs(d - 4.0) < eps:
                N[i].append(j)
    return N

def order_ac(f, nbrs, V):
    cen = V[f]
    out = [c / math.sqrt(dot(cen, cen))
           for c in cen]
    ref = [V[nbrs[0]][k] - cen[k]
           for k in range(3)]
    d = dot(ref, out)
    t0 = [ref[k] - d * out[k] for k in range(3)]
    nt = math.sqrt(dot(t0, t0))
    t0 = [x / nt for x in t0]
    bn = [out[1]*t0[2] - out[2]*t0[1],
          out[2]*t0[0] - out[0]*t0[2],
          out[0]*t0[1] - out[1]*t0[0]]
    def ang(k):
        v = [V[k][i] - cen[i] for i in range(3)]
        d = dot(v, out)
        t = [v[i] - d * out[i] for i in range(3)]
        return math.atan2(dot(t, bn), dot(t, t0))
    return sorted(nbrs, key=lambda k: -ang(k))

def canon(t):
    cands = []
    for s in range(5):
        r = t[s:] + t[:s]
        cands.append(r)
        cands.append(r[::-1])
    return min(cands)

def bracelets():
    seen, out = set(), []
    for p in permutations([1, 2, 3, 4, 5]):
        c = canon(p)
        if c in seen: continue
        seen.add(c)
        out.append(list(p))
    return out

def placements(b):
    out, s = [], set()
    for i in range(5):
        r = b[i:] + b[:i]
        for x in (r, r[::-1]):
            t = tuple(x)
            if t not in s:
                s.add(t); out.append(list(x))
    return out

def solve():
    nbrs = neighbours(ICO)
    ordered = [order_ac(f, nbrs[f], ICO)
               for f in range(12)]
    B = bracelets()
    m = cp_model.CpModel()
    piece = [m.NewIntVar(0, 11, "")
             for _ in range(12)]
    edge = [[m.NewIntVar(1, 5, "")
             for _ in range(5)]
            for _ in range(12)]
    T = [[i] + p
         for i, b in enumerate(B)
         for p in placements(b)]
    for f in range(12):
        m.AddAllowedAssignments(
            [piece[f]] + edge[f], T)
    m.AddAllDifferent(piece)
    done = set()
    for f in range(12):
        for e, g in enumerate(ordered[f]):
            ep = ordered[g].index(f)
            k = tuple(sorted([(f, e), (g, ep)]))
            if k in done: continue
            done.add(k)
            m.Add(edge[f][e] == edge[g][ep])
    m.Add(piece[0] == 0)
    m.Add(edge[0][0] == B[0][0])
    s = cp_model.CpSolver(); s.Solve(m)
    return B, [(s.Value(piece[f]),
                [s.Value(edge[f][e])
                 for e in range(5)])
               for f in range(12)]

The solver returns a tiling in roughly $130$ milliseconds. A sample solution is shown in Figure 9.2: each face is drawn as a pentagon labelled with the face index and the bracelet letter, with the five edge numbers arranged anti-clockwise around its perimeter. The shading is by piece identity; the edge-matching constraint is satisfied across all thirty physical edges.

Sources. John Conway’s puzzle is recorded in the Book of Problems compiled by Conway, Berlekamp and Guy at Cambridge in the late 1970s, and circulates in folklore form from there. The existence of solutions is not obvious from the outset: there are edge-matching puzzles on dodecahedra whose constraint systems are unsatisfiable, and the twelve-bracelet constraint happens to be sufficiently generous. Counting solutions is a harder matter than deciding existence. Enabling parameters.enumerate_all_solutions on the CP-SAT solver counts raw labelled tilings, of which there are in the low thousands; but the two pinning constraints used above do not by themselves quotient out the dodecahedron’s $60$-fold rotation group, so reducing that figure to the number of genuinely distinct solutions would require a full canonical-labelling pass over the $60$ rotations. The solver as written settles the existence question, which is the one Conway posed.