Snake Eggs

Some puzzle rules are local: a cell looks at its neighbours and is content. Others are global, and global rules are what make a puzzle hard to model. The Snake Egg puzzle, set by Serkan Yürekli, has one of each, and the tension between them is a clean doorway into one of the more advanced techniques an integer programmer carries: adding the hard constraints only when the solver tries to break them. That technique is logic-based Benders decomposition, and a grid of snakes and eggs is a gentler place to meet it than a factory.

The puzzle

Draw a snake through a grid: a one-cell-wide path that turns only at right angles, never touching itself, with its head and tail fixed in advance. The cells the snake does not cover must break up into eggs, separate blobs of cells, one egg of each size from $1$ up to some number $n$. Each egg must be a single connected piece, and no two eggs may touch, so between any two eggs runs a length of snake. A few cells are given in advance to pin the answer down.

Our instance is the six by six grid of Figure 32.1, with five eggs of sizes $1$ through $5$. The two ringed ends are the snake’s head and tail; three more cells are labelled with the egg they belong to. Fifteen cells go to the eggs, so the snake is the remaining twenty-one, and the solution drawn is the only one the clues allow.

The easy half of the model

Give each cell $s$ a type: $0$ if it is snake, or the size $k$ of the egg it belongs to. Encode that with binary variables $x_{s,k}$, one for cell $s$ and type $k$, equal to $1$ when cell $s$ has type $k$. Most of the rules are then local and fall out at once. $$\begin{aligned} &\sum_{k} x_{s,k} = 1 &&(\text{every cell has one type}),\\[2pt] &\sum_{s} x_{s,k} = k &&(\text{egg } k \text{ has } k \text{ cells}). \end{aligned}$$ Two eggs must not touch, which is to say no two neighbouring cells carry different egg types; and a snake cell that sits inside the path has exactly two snake neighbours, while each of the two ends has exactly one. Writing $N(s)$ for the neighbours of $s$, $$x_{s,k} + x_{s',k'} \le 1 \quad (s' \in N(s),\; k \ne k',\; k,k' \ge 1),$$ $$\begin{aligned} &\sum_{s' \in N(s)} x_{s',0} = 1 &&(\text{the two ends}),\\[2pt] &2\,x_{s,0} \le \sum_{s' \in N(s)} x_{s',0} \le 4 - 2\,x_{s,0} \ \ &&(\text{other cells}). \end{aligned}$$ The last pair reads as one statement: if $s$ is a snake cell its snake neighbours number exactly two, and if it is not, they are left free. Add the given clues as fixed variables and the model is complete except for one thing, and it is the thing that matters.

The hard half, and the trick

Nothing above forces an egg to be connected, or the snake to be a single path. Solve what we have and the solver cheerfully cheats: it scatters an egg into two distant pieces of the right total size, or pinches off a closed loop of snake far from the head, since a loop also has two snake neighbours at every cell. Connectivity is a global rule, and global rules are expensive to write down. The exact connectivity constraints exist but there are exponentially many of them, one for every subset of cells that could be a stray piece, far too many to hand the solver at the start.

The trick is to not write them down. Solve the cheap model, look at the answer, and if some egg has come apart or the snake has grown a loop, add one constraint that forbids exactly that break, then solve again. A disconnected piece $C$ of egg $k$ is illegal because, being smaller than $k$, it cannot be the whole egg, yet it has no cell of egg $k$ touching it from outside. So demand that it does: $$x_{s,k} \le \sum_{s' \in N(C)} x_{s',k} \qquad \text{for each cell } s \in C ,$$ where $N(C)$ is the rim of cells just outside $C$. The cell $s$ may stay in egg $k$ only if the piece gains an outside neighbour of the same egg, which is to say only if it stops being a stray piece. The same cut, applied to a loop of snake, severs the loop. Each cut kills the current cheat and a whole family of others like it; there are finitely many solutions, so after enough cuts the cheating stops and the answer is genuine.

from ortools.sat.python import cp_model

R = C = 6
EGGS = [1, 2, 3, 4, 5]                # one egg of each size
K0 = [0] + EGGS                       # 0 is the snake
HEAD, TAIL = (0, 0), (2, 2)
CLUES = {HEAD: 0, TAIL: 0, (1, 4): 1, (4, 0): 2, (3, 3): 5}
cells = [(i, j) for i in range(R) for j in range(C)]

def nbrs(s):
    i, j = s
    return [(i+a, j+b) for a, b in ((1,0),(-1,0),(0,1),(0,-1))
            if 0 <= i+a < R and 0 <= j+b < C]

def components(group):                # connected pieces of a set of cells
    group, seen, out = set(group), set(), []
    for s in group:
        if s in seen:
            continue
        stack, comp = [s], {s}; seen.add(s)
        while stack:
            for w in nbrs(stack.pop()):
                if w in group and w not in seen:
                    seen.add(w); comp.add(w); stack.append(w)
        out.append(comp)
    return out

def solve_snake():
    m = cp_model.CpModel()
    x = {(s, k): m.NewBoolVar("") for s in cells for k in K0}
    for s in cells:
        m.Add(sum(x[s, k] for k in K0) == 1)
    for k in EGGS:
        m.Add(sum(x[s, k] for s in cells) == k)
    for s, k in CLUES.items():
        m.Add(x[s, k] == 1)
    for s in cells:
        for ss in nbrs(s):            # no two eggs touch
            for k in EGGS:
                for kp in EGGS:
                    if k != kp:
                        m.Add(x[s, k] + x[ss, kp] <= 1)
        if s in CLUES and CLUES[s] == 0:           # the two snake ends
            m.Add(sum(x[ss, 0] for ss in nbrs(s)) == 1)
        else:                                       # other cells: degree two
            m.Add(sum(x[ss, 0] for ss in nbrs(s)) >= 2 * x[s, 0])
            m.Add(sum(x[ss, 0] for ss in nbrs(s)) <= 4 - 2 * x[s, 0])
    sv = cp_model.CpSolver()
    while True:
        sv.Solve(m)
        typ = {s: next(k for k in K0 if sv.Value(x[s, k])) for s in cells}
        cut = False
        for k in EGGS:                              # eggs must be connected
            for comp in components([s for s in cells if typ[s] == k]):
                if len(comp) < k:
                    rim = {w for s in comp for w in nbrs(s)} - comp
                    for s in comp:
                        m.Add(x[s, k] <= sum(x[w, k] for w in rim))
                    cut = True
        for comp in components([s for s in cells if typ[s] == 0]):
            if HEAD not in comp:                    # snake loops are illegal
                rim = {w for s in comp for w in nbrs(s)} - comp
                for s in comp:
                    m.Add(x[s, 0] <= sum(x[w, 0] for w in rim))
                cut = True
        if not cut:
            return typ

The loop returns the unique solution of Figure 32.1, the master problem solved a handful of times, each pass adding a few cuts where the previous answer had cheated.

Why this is Benders

The shape of that loop is the whole idea of Benders decomposition. Split a hard problem into an easy master, here the local rules, and the awkward remainder, here connectivity. Solve the master, which is optimistic because it ignores the remainder; test its answer against the part left out; and if the answer fails, feed back a cut, a new constraint that the master must honour next time. Because each cut removes the latest bad answer and many like it, the master is dragged, pass by pass, toward an answer that survives the test. When the test is a question of feasibility rather than cost, as connectivity is here, the cuts are feasibility cuts and the method is the logic-based Benders decomposition of Hooker. The snake teaches it without a single dual variable: omit the hard constraints, and reintroduce them only where the solver is caught breaking them.

There is a second way to force connectivity that adds everything at the start instead. Pick one source cell in each egg and let it send a unit of flow to every other cell of that egg along a network laid over the grid; flow can only reach a cell that is genuinely linked to the source, so an egg that arrives intact is an egg that is connected. This flow model is compact, a fixed and polynomial set of constraints rather than a growing one, and it needs no loop. It is the tidier object on the page. But the authors who set this puzzle found the lazy loop the faster solver, because the cuts that connectivity actually requires are far fewer than the flow variables laid down in advance for the connections it might have needed. Tidiness and speed part ways, and the lesson is to know which you are buying.

What the puzzle teaches

A model is allowed to be incomplete on purpose. The instinct drilled into a beginner is to state every rule before pressing solve, but some rules are cheap to state and some are ruinous, and the ruinous ones are often the global ones: connectivity, no subtours, no overlaps across time. The mature move is to leave those out, solve the cheerful relaxation, and let the solution itself tell you which of the exponentially many missing constraints you actually needed. That is the discipline behind subtour elimination for the travelling salesman, behind cutting planes generally, and behind Benders. The snake and its eggs are small enough to watch it happen: the first answer cheats, a cut is drawn around the cheat, and a few honest passes later the grid is full.

Sources. The puzzle, its integer-programming model, the multicommodity-flow approach to connectivity, and the lazy-constraint approach with its disaggregated feasibility cuts all follow Mitchell Harris and Michael Forbes, The Snake Eggs Puzzle: Preparing Students for Benders Decomposition, INFORMS Transactions on Education volume $23$, number $3$ ($2023$), pages $210$–$217$, published open access under a Creative Commons Attribution licence; the cut used above is their disaggregated form, proved exact in their appendix. The instance solved here is our own, with a unique solution under its clues, confirmed by the model. The puzzle itself is by Serkan Yürekli (Grandmaster Puzzles, $2016$). Logic-based Benders decomposition is due to John N. Hooker; see J. N. Hooker and G. Ottosson, Logic-Based Benders Decomposition, Mathematical Programming volume $96$ ($2003$), pages $33$–$60$, and the classical method to Jacques F. Benders, Partitioning Procedures for Solving Mixed-Variables Programming Problems, Numerische Mathematik volume $4$ ($1962$), pages $238$–$252$.