This document describes the programming project for the Fall 2024 edition of ECEN 2703.

1 Introduction

In our treatment of logic, we have learned how to solve knights-and-knaves puzzles. We have also seen how to apply logic to the Minesweeper problem. The Z3 tutorial that you read shows how to solve Sudoku puzzles by encoding the constraints that every row, column, and 3 × 3 box of the grid must contain the digits 1 through 9. For our programming project, we take on two pencil puzzles, in which the solver has to trace paths that satisfy given constraints on a rectangular grid.

Example 1. In a Sloop (simple loop) puzzle, we are given a rectangular grid. Some cells contain a square as in the 6 × 6 grid below.

We need to trace a simple loop (a loop that does not cross itself) that visits all the cells without a square in them. The loop must go through the center of each cell it visits and must move either horizontally or vertically. It must not touch itself, which is to say that it can cross a cell at most once.

The solution to the puzzle above is shown below. (We say “the solution” because in well-designed puzzles the solution is unique.) The inside and outside of the loop are shaded differently to make the graphics easier to read.

For an experienced solver, this is an easy puzzle, but if this is the first sloop puzzle you’ve ever come across, you may want to cover the solution and see if you can re-discover it. Later, we’ll talk about “tricks of the trade” that help humans to tackle sloop puzzles. In any event, even if a puzzle baffles you, it is straightforward to check that a purported solution is indeed correct. (You should try it on the solution above.) Showing that a solution is unique is more involved. More on this in Section 6.

Example 2. Slitherlink puzzles share the basic setup of Sloop puzzles—a grid in which we need to draw a simple loop that does not touch itself—but have different rules. The loop must be formed by the edges of the cells. A clue in a cell is the number of edges of that cell that participate in the loop. Here is an example:

The (unique) solution is shown below. As in Example 1, colors are used to improve readability.

Again, it is not difficult to verify that the solution is correct. For instance, it’s easy to check that the loop uses k edges of each cell that contains k.

Slitherlink has more complex rules than Sloop. We’ll start from the latter so that we can “learn the ropes.” Solving Sloop will teach us how to deal with connectedness constraints. This ability will make the task of solving Slitherlink easier. It will also help with variants of Sloop and Slitherlink, as well as with other puzzles that deal with loops like Masyu and Yajilin.

These notes aim to be self-contained. If you want to know more, though, there’s plenty available in print and on the Web. Among the books, it’s worth citing Knuth [6, pp. 177-178], and Hearn and Demaine [3, p. 177].

2 Tricks of the Trade

While in principle one could write a solver for one of our puzzles without having ever tackled one puzzle, some familiarity with the manual solution process will definitely help. Hence, in this section, we look at some of the basic techniques on which human solvers rely.

2.1 Solving Sloop Puzzles

There are two observations whose application helps us solve an example of Sloop puzzle like the one of Example 1.

Figure 1: Stages in a solution of the Sloop puzzle of Example 1.

• If an empty cell has only two neighbors through which the loop may go, then the loop goes through those neighbors. For example, an empty cell in a corner of the grid, and an empty cell along the border and next to a black square, have two neighbors each. Moreover, if the loop already goes in and out of a cell, that cell is no longer available as neighbor of another cell (to which it is not already connected).

• When extending the path to eventually form. a loop, one must carefully avoid entering cul-de-sacs and prematurely closing the loop. A cul-de-sac is a region of the grid where the path, once entered, does not have enough maneuvering space to get out again. The simplest example is a cell with only one available neighbor left. A loop is closed prematurely when it does not visit all empty cells.

These observations often help a solver to make progress in the solution. For example, Figure 1 shows how the Sloop puzzle of Example 1 may be solved. The rule about cells with two neighbors takes us from the initial grid to its right neighbor. Then, we observe that, if the path were extended from r2c1 (Row 2, Column 1) to the right, a small loop—one that does not visit all the empty cells—would result. Therefore, the path must continue downward from r2c1 to r3c1. This gives the rightmost grid in the top row of Figure 1.

We now observe that r3c2 has only two available neighbors left: r2c2 and r3c3. The path is extended accordingly. Now, the same observation applies to r2c3. After we have extended the path from it to r3c3 and r2c4, we can apply the same trick to r4c3 to obtain the left grid in the bottom row of Figure 1.

We now turn our attention to r3c4, which has two available neighbors left: r3c5 and r4c4. We let the path through r3c4 connect those neighbors. We

Figure 2: Stages in the solution of the Slitherlink puzzle of Example 2.

also notice that r5c5 still has three neighbors available. However, if we ran the path through it from r5c3 to r5c6, we would close a small loop. This means that the path must go through the third neighbor, connecting r5c5 to r4c5.

This gives the center grid of the bottom row. There, we observe that we cannot extend the path from r3c5 to r3c6, lest we should close the loop pre-maturely. The two free ends of the path in Row 3 must be extended downward. The only available moves then complete the solution.

Note how the systematic application of rules and observations derived from them eliminated the guesswork: we never had to say, “let’s extend the path this way and see what happens.” Many puzzle enthusiasts subscribe to the idea that a good puzzle is one that can be solved by an experienced human solver without any bifurcation. In Computer Science, we’d say, “without backtracking.”

2.2 Solving Slitherlink Puzzles

The most commonly used tricks to solve Slitherlink puzzles include those that we saw for Sloop. That is, one checks for locations in the grid where the loop can only be extended in one way. Moreover, when extending the path, choices that would create multiple loops, loops that cross themselves, paths that cannot be closed to form. loops, or branching paths can be safely discarded. In addition to these criteria, Slitherlink has a number of “tricks” that look for patterns in the clues. Let’s see some common techniques at work in the solution of the Slitherlink puzzle of Example 2. There are too many tricks to see them all at work in one example, but we’ll get the idea.

First, we mark all the edges surrounding cells with a 0 in them because they cannot be part of the loop. It is customary to use small ×’s to mark unavailable edges, so that it’s easy for human solvers to see where they know that the path may not go.2 If we systematically marked all the edges that are not on the loop with an ×, at the end of the process every edge would be either part of the loop or marked. We won’t do that. Instead, we’ll only mark an edge if we deem that a reminder of its unavailability will help us.

Next, we observe that, if two adjacent cells both have 3 in them, then, in a large enough grid, the loop must take the edge that separates them and the two edges parallel to it, as in r2c1 and r2c2 of our example. This is an example of a pattern in the clues that a solver looks for. To see why we are justified in selecting those three edges, let’s start from the edge between the two cells. If it weren’t part of the loop, then the loop would have to use the remaining six edges to satisfy the constraints. That would produce the following situation:

If there are other clues different from 0 in the grid (this is what we meant by “large enough grid”) this loop cannot be the solution. Having established that, in our example, we need the loop to pass between r2c1 and r2c2, we now consider the edge to the left of r2c1. If it were not part of the loop, we’d have the following situation:

The ×’s are there because a corner of a cell cannot have more than two edges incident on it that are part of the loop. If if did, the path would either branch (with three edges) or touch/intersect itself (with four edges). The two ×’s tell us that we cannot select three edges around the three on the right unless we have the edge to the left of the three on the left. The argument for needing the edge to the right of r2c2 is essentially the same.

With similar reasoning we could prove that a 3 that shares a corner with another 3 makes the loop use the two sides that don’t touch that corner.

(What would happen if the loop used both edges of one cell with a 3 incident on the shared corner?)

The observations we’ve made so far give the middle grid of the top row in Figure 2. Let’s now focus on the top-left corner of r1c5. It has three incident edges, two of which are known not to be on the loop. (They are marked.) If the path used the remaining edge (the one above r1c4) it would reach a dead end. Hence, the edge above r1c4 is marked with an ×. With similar argument we mark the edges above r1c6 and to its right.

Let’s now turn our attention to r5c5. If the edge above it were in the loop, the edge to its left would give the only possible extension of the path from the left endpoint. However, this would put two edges around a cell with a 1 in it, violating the clue constraint. By similar argument, we conclude that the edge to the left of r5c5 is also to be marked.

Next, we look at r3c3 and notice that if the loop used its right edge, it would also have to use its bottom edge to “get out.” Since the cell contains a 1, we conclude that its right edge not on the loop and we mark it. Likewise, the bottom edge of r3c3 is not on the loop and we mark it. When this is done, we notice that there are only two edges left to satisfy the constraint on r3c4; hence, we add those edges to the path.

Now, however, the bottom-left corner of r2c5 has two incident edges on the loop: we can mark the other two with ×’s. This means that the only edge left to satisfy the clue in r2c5 is the one to its right. The path must extend from both ends of this edge without closing prematurely. When this is done, we have the rightmost grid in the top row of Figure 2.

Moving on, we now look at the bottom-right corner of r3c4. The path must extend from there and the only possible direction is to the right, by including the edge below r3c5. From the bottom-right corner of r3c6, the path can only extend downward to the bottom-right corner of r4c6. From there, it cannot go left, because, then, it would have to go down, taking two sides of a cell with a 1 in it (r5c5). Therefore, the path takes the right edge of r5c6, and then goes down again because it has already used the one allowed edge around r5c6.

From the bottom-right corner of the grid, the path can only go left, passing below r6c6. At this point, we notice that the edge between r5c5 and r5c6 is not on the loop. If it were, it would be impossible to extend the path from its upper end. This means that the edge around r5c5 that is on the loop is the one below it. The only way to connect it to the free end in the bottom-left corner of r6c6 is via the edge to the left of that cell.

We now turn our attention to r4c3 and notice that there are only two edges left to satisfy its constraint. Hence, we add the edges to the left and below r4c3 to the path. The top-right corner of r5c2 now has two incident edges on the loop; hence, we mark the other two.

The interesting question to ask, at this point, is which of the two available edges around r3c3 is to be on the loop. Either way, the path extends around the 3’s in r2c2 and r2c1 until it reaches the top left corner of r2c1. Suppose it were the top edge of r3c3 that is selected. Then, the path would be trapped in a dead end and could not connect to the free end below r5c5. Hence, the loop must include the left edge of r3c3. Since the top-left corner of r3c3 now has two incident edges on the loop, we mark the other two. This gives us the first grid of the bottom row in Figure 2.

As we remarked in the last paragraph, the path must now extend to the top-left corner of r2c1. From there, it can only go up and then right until it reaches the top-left corner of r1c4. It cannot take the edge below r1c4 because that would lead to a dead end. (So, we mark that edge.) Therefore, from the top-left corner of r1c4, the path must turn down until it connects to the free end at the top-left corner of r3c4. We have reached the situation described in the middle grid of the bottom row in Figure 2.

The path now has two free ends that must be connected. Clearly, from the top-left corner of r5c4, the path can only go down. If it then went down again or turned right, the loop would be closed prematurely: it would not include edges of either r5c2 or r6c2. Hence, the path must go left. At the top-right corner of r6c2 it must go left again for similar reason. From the top-left corner of r6c2 it has to turn back to join the other free end. It cannot do so right away, though, because it would then use three edges around a cell that holds a 2. Hence, the path reaches the left edge of the grid, turns around, and crosses below r6c2, continuing until the bottom-left corner of r6c5. The last step is to close the loop by taking the left edge of r6c5.

It should be clear that this is one of the possible sequences of steps that may be taken to solve the puzzle. It does illustrate, though, the type of (often subtle) reasoning that Slitherlink puzzles often require of human solvers. Mechanical solvers, like Z3, may not know all the tricks, but—fortunately for us—have brute force to spare.

3 Forcing a Single Loop

In Sloop and Slitherlink, we need to make sure that there is a single loop. In our solvers, we need to specify appropriate constraints for Z3. We adopt an approach based on [1, 2], whose main ideas we summarize here.