Solving Sloop and Slitherlink with Z3

September 13, 2024

Abstract

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.

Let’s look at the two loops below and suppose that we go around them in clockwise fashion, as shown by the arrows. (We’ll stick to clockwise travel throughout.)

The loop on the left contains four turns, while the loop on the right contains eight turns. We identify these turns by the directions before and after the turn. Let’s focus on two types of turns: up-then-right (marked by orange circles) and right-then-up (marked by green squares). Let’s call these turns notable. In the loop on the left, there is one up-then-right turn and no right-then-up turns. In the loop on the right, there are two turns of the first type and one turn of the second. A few more examples will convince you that in every (clockwise) loop there is always one more up-then-right turn than there are right-then-up turns. So, the number of notable turns is always odd. Intuitively, the turns of the second type counter the attempt of the turns of the first type to close the loop. Since the loop closes, the turns of the first type must have the last word.

It is also not difficult to see that one cannot take two up-then-right turns without an intervening right-then up turn. Hence, the difference between the numbers of notable turns of the two types is always 0 or 1 along the loop and is 1 at the end. This suggests that we can track this difference with just one bit. (More details and actual proofs of all these claims are found in [1, 2].)

Let’s see how to convert this idea into constraints for Z3. We associate one Boolean variable to each cell of the grid. We then impose constraints saying that, if the loop turns up-then-right or right-then-up in that cell, the turn-tracking variable of this cell must have opposite value to that of its predecessor along the path. In the remaining 10 ways in which the loop goes through a cell, the turn-tracking variable must have the same value as the variable from the predecessor cell. The turn-tracking variables of the cells not on the loop will take arbitrary values and will be of no concern to us.

The chain of constraints around a loop forces the turn tracking bit to change an odd number of times: If there are n > 0 up-then-right turns, there are n − 1 right-then-up turns, and 2n − 1 is always odd. If nothing is done about it, this means that the constraints are unsatisfiable! This apparent problem turns out to be the key to guarantee that there exactly one loop. The clever idea is to allow exactly one exception to the constraint in the whole grid. Then, one loop satisfies the constraints, but zero or more than one loops do not. In Sections 4 and 5 we’ll see how to incorporate this technique in our encoding of the Sloop and Slitherlink puzzles.

4 Modeling Sloop Puzzles

We now discuss how to model a Sloop puzzle for Z3. With minor adaptations, what we say applies to other SAT and SMT solvers, but we’ll focus on our favorite tool.

For an n×m grid, with cell (0, 0) in the top-left corner, we have (n+1)(m+1) cell corners—from (0, 0) to (n, m). We assume that corner (0, 0) is the top-left corner of cell (0, 0) and corner (n, m) is the bottom-right corner of cell (n − 1, m − 1). (See Figure 3.) The four corners of cell (i, j) are (i, j), (i, j + 1), (i + 1, j), and (i + 1, j + 1). We’ll keep this convention for Slitherlink too.

Recall that the loop in Sloop puzzles goes through the centers of the empty cells. We associate one variable, fi,j to each cell corner and one variable, pi,j ,

Figure 3: Cell and corner indexing conventions for n = 3 and m = 4.

to each cell of the grid. If fi,j is true, then corner (i, j) is inside the loop; otherwise, it is outside the loop. The value of pi,j is the parity around the loop that was discussed in Section 3.

Let’s start with the constraints on the f variables.

• The corners along the perimeter of the grid are all outside the loop. That is, the f variables around the border of the grid are all made “false” by the constraint (¬fi,j ). So, there are only (n − 1)(m − 1) corners whose variables Z3 can play with to find a solution. While it is possible to avoid creating variables for the corners along the grid’s border, doing so complicates writing the constraints. Hence, we’ll define variables for all (n + 1)(m + 1) corners and then fix the values for the 2(n + m) corners around the border.

• The cells with black squares are either entirely inside the loop, or entirely outside the loop. Hence, the f variables for their four corners are either all true, or all false.

• Every empty cell is traversed by the path. This means that at least one of its corners is inside the loop and at least one of its corners is outside.

• Every empty cell is traversed by the path once. This forbids checkerboard patterns in the four corner variables. It is not possible for the north-west and southeast corners to be inside while the northeast and southwest corners are outside, or vice versa.

If these constraints on the f variables are satisfied, but the constraints on the p variables are ignored, we get a weak solution. In a weak solution, all empty cells are on a loop, and all cells with squares are either entirely contained in some loop, or entirely outside every loop, but there may be multiple loops. To avoid multiple loops is the purpose of the p variables.

Figure 4: Possible values of the p variables for the puzzle of Example 1. The exception to the parity constraint occurs at cell (0, 0), where the value of the p variable does not change, even though the loop takes an up-then-right turn.

As we said, we associate to each cell a Boolean variable pi,j , which switches value whenever the loop takes an up-then-right or right-then up turn. We do not insist on the particular values of the p variables: only on their relations to the neighboring variables if they are on the loop. In particular, if the values of all the p variables around the loop are flipped, from a valid solution we get another valid solution to the constraints (while the solution to the puzzle does not change).

As discussed in Section 3, we must grant one exception to the parity con-straint at one location around the loop. In Sloop, we can fix where the exception is granted because we can identify in advance a cell through which the loop goes. Indeed, any empty cell can be chosen as the exceptional one.

For the puzzle of Example 1 (n = m = 6), Figure 4 shows possible values: The f variables inside the loop are true; those outside are false. Each cell is annotated with the value of its p variable: red means true and light blue means false. To reduce clutter, the values of the p variables are only shown for the loop corners. Notice that the solver could have reversed the assignment of truth values to the p variables. For us, a puzzle with unique solution will be one for which the loop cannot be changed without violating the constraints. We will not insist on the uniqueness of the assignment to p variables.

4.1 Encoding the Rules of the Puzzle

We now look at how to translate the given clues into constraints on the f variables. (The p variables are used to get the right shape of the loop, but do not appear in the constraints due to the clues.)

The key observation is that, if the loop goes through a cell, then one or more corners are inside the loop, and one or more corners are outside. Specifically, if the loop goes straight through the cell, then two (adjacent) corners are inside and the other two are outside. If the loop turns in the cell, then three corners are inside and one is outside, or vice versa. If the loop does not go through a cell, the four corners will be either all inside or all outside. In the examples below, a filled square on a cell corner signifies that the corner is inside the loop, while an empty square signifies that the corner is outside the loop.

The arrows indicating the direction of travel are based on our convention that we go around the loop clockwise, so that the outside region is always on our left. Of the 16 possible combinations of “inside/outside” for 4 corners, 4 correspond to straight paths through the cell; 8 correspond to turning paths; 2 correspond to the path not going through the cell; and 2 are impossible under the Sloop rules because they would require the path to cross the cell twice. (You should draw all 16 patterns to familiarize yourself with this idea. Your diagram will help you when you code the constraints.)

The other mandatory part of the constraints has to do with guaranteeing a single, simple loop. We follow the approach outlined in Section 3. Recall that we can tell what the loop does in cell (i, j) if we know the values of the four corner variables fi,j , fi,j+1, fi+1,j , fi+1,j+1. In 12 of the 16 cases, the loop goes through the cell. In each of these cases, we know which cell it comes from and which cell it visits next. Hence, we know whether it takes an up-then-right turn, it takes a right-then-up turn, or does something else. In the first two cases, we impose the constraint that pi,j should have the value opposite to the p variable of the predecessor; in the last case, we impose the constraint that pi,j has the same value as the t variable of its predecessor. For the 4 combinations of the corner variables that do not correspond to cells on the loop, we specify no constraints on the p variables. As an example, consider this case:

(i, j) (i, j + 1)

For these values of the f variables, the constraint on the p variables should be,

(pi,j ≠ pi+1,j ) ∧ (pi,j+1 = pi,j ) .

Therefore, we need the constraints,

(¬fi,j ∧ ¬fi,j+1 ∧ ¬fi+1,j ∧ fi+1,j+1) → pi,j ≠ pi+1,j

(¬fi,j+1 ∧ ¬fi,j+2 ∧ fi+1,j+1 ∧ fi+1,j+2) → pi,j+1 = pi,j .

We also need other constraints: for each cell, one constraint for each of the 12 combinations of corner values that are possible at that cell. In practice, we want to loop over all cells and add up to 12 constraints for each of them. Why do we say “up to?” Because, for example, in the top row of the grid, the loop cannot enter or leave a cell from above. Trying to refer to the cell above a cell in the top row would cause an out-of-range access, which is not nice.

As discussed in Section 3, we need to allow one exception to the p constraints. That is, we need to let the constraints be ignored in exactly one cell. In general, we may want to let the solver pick the location by associating a Boolean variable, ei,j , to cell (i, j). (See [1] for the details.) In fact, for Slitherlink, we’ll do it. However, for Sloop we know that the loop has to traverse all the empty cells. Hence, we can pick any one empty cell and skip that cell when adding the single-loop constraints. We can also fix the value of the p variable for the exception cell. In Figure 4, we see that the p0,1 = p0,0, which is against the constraints. In fact, the first empty cell encountered when scanning the grid was chosen as the place where to make an exception.

4.2 Why Do We Get One Simple Loop?

In this section we explain why the constraints we impose guarantee a single loop. We start by summarizing the constraints that we impose.

For each cell in the grid, except for the exceptional one, the solver should be passed the up-to 12 constraints on the p variables corresponding to the possible configurations of the cell’s four corners.

In addition, there is a constraint for each cell that forbids checkerboard patterns for the cell’s four corners. Moreover, all the corners along the edges of the grid must be false. Finally, we need to assert that at least one cell corner is inside the loop.

We now prove that, for the constraints described above, a solution must consist of one simple loop. Consider an assignment of values to all f variables that satisfies all the constraints. This assignment fixes what the path does in each cell. Hence, it constrains the values of the p variables of the cells along the path.

If no cell is on the path, then it is impossible to have one corner inside the loop and the grid border outside the loop. So, at least one cell is on the path. If a cell is on the path, its predecessor is also on the path because the two corners along the edge that connect the two cells have different values. The predecessor of the predecessor must also be on the path—for the same reason. Since the grid is finite, at some point, in going from one cell to its predecessor, we must come back to the cell we started from. Hence, we have a loop.

Note that the no-checkerboard constraints prevent the path from branching or intersecting itself. Hence, as we walk from each cell on the path to its predecessor, we must reach the cell we started with before any other cell we subsequently visited. Hence, each loop we trace is simple.

So far, we have shown that in any solution there must be a loop and that all loops are simple. However, there may be multiple loops. This is where the p variables come into play. The constraints on the p variables are such that, if all cells along a loop obey them, there’s an odd number of changes. That implies a contradiction because we assumed that the constraints were satisfied. However,

Figure 5: Cuts are crossed an even number of times by the loop.

with the one exception that we have, we can avoid the contradiction for one loop—and only for one. In conclusion, there must be at least one simple loop, but there cannot be more than one. Hence, there is exactly one simple loop.

4.3 Optional Constraints

The optional constraints can be ignored in an initial implementation. If your solver is fast without additional constraints, you can ignore them altogether. For larger puzzles, however, they may make a difference. The optional constraints may guide Z3’s search for a solution by giving early warning that certain as-signments to part of the variables cannot be extended to full assignments that satisfy the constraints. If you need them, you may want to introduce them one at a time once your initial implementation works, so that you can verify that they speed up the solver without changing the solutions.

A class of optional constraints deals with impossible patterns in the f vari-ables. Consider Figure 5. Note that the loop crosses the red vertical line and the green rectangle an even number of times. This observation is true in general of every line that runs on the grid lines and divides the grid into two regions. For the vertical line, there is a left region and a right region. For the rectangle, there is a region inside the rectangle and one outside. We can say even more. If we walk around the loop so that the outside of the loop is always on our left, then we cross the vertical line three times going from left to right and three times going from right to left. At the same time, we enter the green rectangle twice and also exit twice.

Any valid solution to a Sloop puzzle satisfies these cut constraints. In the puzzle below, the red cut may be passed in three places: r2c1, r2c4, and r2c6.

However, the loop must cross the red cut twice because 3 is, obviously, odd. We cannot avoid the two passages in Columns 1 and 6; otherwise, we would create dead ends. Hence, the loop cannot go from r2c4 to r3c4. This conclusion allows us to draw the loop segment shown on the right below.

We can add cut constraints to the solver to let it stop working on a partial solution that is guaranteed to break them. Of course, there are many horizontal and vertical cuts, and even more closed lines in the grid. So, we will typically limit ourselves to a few, uniformly spaced, cuts. For a vertical cut like the red line of Figure 5, we ask whether the number of times ¬fi,5 ∧ fi+1,5 is satisfied equals the number of times fi,5 ∧ ¬fi+1,5 is satisfied, when i goes from 0 to 10.

Another technique that is important for human solvers is based on even and odd cells. This technique is known as parity, but is a different application parity from the one we rely on to guarantee a single loop. Cell (i, j) is even if i + j is even, and is odd otherwise. An even cell has odd neighbors and vice versa. Hence, the loop visits even and odd cells in alternation. This means that a solvable puzzle must have the same number of even and odd empty cells. Take the puzzle of Example 1. There are 18 even cells and 18 odd cells in the 6 × 6 grid. Of the 4 black squares, two are on even cells (r1c3 and r4c2), while the other two are on odd cells (r2c5 and r6c3). This puzzle passes the parity check.

A puzzle that fails this parity check is unsolvable. If is passes, it may or may not be solvable. In the grid below, even cells are shaded in green. The puzzle has 11 even empty cells and 11 odd empty cells: it passes the parity check. However, r1c1 has only one neighbor; hence, the puzzle has no solution.

So far, we have considered cell parity as a way to detect some unsolvable puzzles, which may be useful to those who set puzzles. We can also use it to make inferences in solvable puzzles like the one below.

The loop has to enter and exit the 3×3 region with the red border at least once because it has to visit all empty cells. There are only three cells in the region where the loop may cross in or out (r4c2, r4c3, and r6c3). Hence, the loop enters and exits exactly once. Moreover, there are equal numbers of even cells and odd cells in the 3 × 3 region. Hence, the loop’s entry and exit points have different parities (i.e., different colors). This means that one endpoint is r4c2, which is the only option for its color. The other endpoint must be r6c3 because the black square in r5c4 forces the path through r6c4. From this, we deduce the fragments of loop shown above on the right. (Note that there are only two neighbors left for r4c3 once it is ruled out as an endpoint.) Joining this path to the one derived with the cut constraint, we get the complete solution.

The puzzle that we have used to illustrate the use of cuts and cell parity is an easy one. Using these advanced techniques on it may feel like taking a sledgehammer to a peanut. For difficult puzzles, though, the situation may be quite different. As far as mechanical solvers are concerned, cell parity suffers from the same drawback as cut constraints: there are many regions to which it may be applied and it’s not obvious which regions yield useful inferences.

To illustrate, in the example above, we could also consider the last two rows of the grid and notice that they contain six white cell and five green cells that need to be on the path. Hence, the loop must enter and exist that region from white cells, namely, r5c3 and r5c5. We would get the same path segment we got with the region within the red contour above. However, if we looked at the two rightmost columns before we traced any path, we could not immediately say whether the loop enters and leaves the region once or twice; consequently, we wouldn’t make much progress.

5 Modeling Slitherlink Puzzles

In Slitherlink, as in Sloop, we want to divide the grid into two regions: inside the loop and outside the loop. A lot of what we have said about Sloop applies to Slitherlink too. Hence, this section is much shorter than the previous one.

The loop, however, uses the edges of the cells, instead of going through the cells’ centers. Therefore, we associate the f variables to the cells themselves instead of the cells’ corners: fi,j , is true if, and only if, cell (i, j) is inside the loop. Conversely, the p variables are associated with the cells corners because it is the cell corners, instead of the cell centers, that are found around the loop.

5.1 Encoding the Rules of the Puzzle

We need to express the constraints on the number of loop edges around cell (i, j) in terms of the f variables. So, we need to understand whether an edge is part of the loop from the f variables of the cells that share that edge. Let’s denote the edges by the cardinal directions North, East, South, and West.

Let’s take the North edge of Cell (i, j) as example; it is part of the loop if:

• The cell is in the first row (i = 0) and it is inside the loop (fi,j is true), or

• The cell is in any row except the first and fi,j ≠ fi−1,j .

Similar observations apply to the remaining three edges. Hence, for each cell, we have four propositions, each for one edge. If the clue in the cell is k, we impose the (pseudo-Boolean) constraint that k of these propositions should be true. If there is no clue in the cell, no constraint is imposed.

Note that, if we imagine that there is a border of cells around the actual grid, and we assume that the border cells are outside the loop, then, when in the first row of the actual grid, we can still write fi,j ≠ fi−1,j .

Next, we need to impose constraints on the p variables. Conceptually, they are the same constraints as for Sloop. Specifically, we still have to consider up to 16 cases, two of which must be forbidden. In practice, there’s a couple of points to be noted.

• The roles of corners and cells are swapped.

• We lack the easy rule to fix where the exception to the parity constraints should be granted.

A general solution to the latter problem is to introduce one Boolean variable for each corner, ei,j which is true if, and only if, that corner is the exceptional one. We then impose the constraint that at most one of these variables is true. We can also impose the constraint that pi,j must be true if ei,j is true.

For the puzzle of Example 2 (n = m = 6), Figure 6 shows possible values of the p variables. Considerations similar to those made for Sloop apply here. We do not insist on the values of the p variables: only on whether they change or stay the same as we go around the loop.

Figure 6: Possible values of the p variables for the puzzle of Example 2. The exception to the parity constraint occurs at corner (1, 0) , where the values of the p variables change, even though the loop does not take either an up-then-right or a right-then-up turn.

6 How Hard Are these Puzzles?

This section will make more sense once we have covered Section 3.3 of our textbook. On first reading, you may skim it, or even skip it.

We have discussed complexity classes for decision problems: those that have yes/no answers. We can derive decision problems from our puzzles by asking, “Does this puzzle have at least one solution?” Notice that we ask for “at least one” instead of “exactly one.” These decision problems are the ones whose hardness we briefly discuss in Section 6.1. The uniqueness question, which is an important one for puzzle setters, is then the subject of Section 6.2.

6.1 Existence of a Solution

If we are given a purported solution to either a Sloop puzzle or a Slitherlink puzzle, we can easily check whether it is indeed a solution. Verifying that no black square is traversed by the loop and every empty cell is, for example, can be done in time linear in the size of the grid. For the connectedness checks, we can build a spanning tree of the inside of the loop in linear time. (The code described in Section 7 already does that.)

All this means that both Sloop and Slitherlink are in NP: a “yes” answer comes with a witness (namely, the solution to the puzzle) that can be checked in polynomial time.

Both problems have been shown to be NP-complete. Sloop is nothing but the Hamiltonian circuit problem for grid graphs, which was proved NP-complete in [4]. T. Yato demonstrated a polynomial-time reduction from the Hamiltonian circuit problem for a restricted class of graphs (known to be NP-complete) to Slitherlink [13, 14]. The proofs of NP-hardness can be found in the references. (See also [9, 10].) Figure 8 shows the puzzle that results from asking whether the graph of Figure 7 has a Hamiltonian circuit. (The example comes from [13].)

Note that it is not enough to say, “Sloop asks the solver to find a Hamiltonian circuit in a graph. The Hamiltonian circuit problem is NP-complete [5]; hence, Sloop is NP-complete.” We actually need the result of [4] because, in principle,

Figure 7: A planar graph with degree at most 3 (left) and its embedding in a grid (right). The graph on the left is planar because it can be drawn without edge crossings. Its degree is at most 3 because every vertex is connected to at most three other vertices. A Hamiltonian circuit is a closed path in the graph that visits each vertex exactly once. One such path is highlighted. Note that the grid on the right does not have a Hamiltonian circuit. Instead, the highlighted path is a closed path that visits each black vertex exactly once.

Figure 8: Reduction from Hamiltonian Circuit to Slitherlink applied to the planar graph of Figure 7. The 6×6 squares delimit the gadgets that are stitched together to encode the grid. Each gadget corresponds to one vertex of the grid. The Hamiltonian circuit found in this solution of the Slitherlink puzzle (one of three solutions) is the one highlighted in Figure 7.

restricting the graphs to grids may exclude the hard cases that make the problem NP-complete. For example, if we further restricted the possible grids so that there are no black squares, the problem would be in P. (See [4, 12] for the details.)

What does the NP-completeness of our puzzles mean for our project? Since no known algorithm for an NP-complete problem runs in polynomial time in the worst case, we should expect to come across puzzles that take an inordinate amount of time to solve. We should expect the transition from easy to very difficult to be abrupt, and we’ll encounter puzzles of the same size that take very different amounts of time to solve. It is quite possible for a minor change in the way we write the constraints to make a large difference in the solution times of some puzzles. All this notwithstanding, most puzzles that are doable by humans are within the (easy) grasp of even a simple solver. Be prepared, but don’t lose heart.

Most people will agree that it is much easier to find a Hamiltonian circuit directly on the graph of Figure 7 than to solve the Slitherlink puzzle of Fig-ure 8. In fact, anyone who is familiar with the definition of Hamiltonian circuit is likely to find one for the graph of Figure 7 in a matter of seconds. The greater difficulty of solving the puzzle is due, at least in part, to the fact that the reduc-tion of Figure 8 produces, for a graph with n vertices (and no more than 3n/2 edges), a grid with O(n 2 ) cells. In proving NP-hardness, we only need to come up with a polynomial reduction scheme. We don’t need a linear reduction. If, hypothetically, we devised a quadratic algorithm to find a solution of a Slith-erlink puzzle, the reduction of Figure 8 would give us a quartic algorithm for Hamiltonian circuit of planar graphs of degree at most 3. Quartic (O(n4)) is much worse than quadratic ((O(n 2 )), but is still polynomial. Recall that reduc-tions like this are not meant to provide practical ways to solve problems: they are only meant to prove that a polynomial algorithm for the candidate problem would yield polynomial algorithms for all problems in NP.

6.2 Uniqueness of the Solution

For most puzzles, including Sloop and Slitherlink, the solution should be unique. We need to extend the basic framework of computational complexity, which talks about decision problems, if we want to talk about how hard it is to check whether a solution is unique. Unsurprisingly, this extension has been done. The starting point is the definition of function problems, in which the result is a string instead of a yes/no answer. The function problem analog to SAT asks for a satisfying assignment to a propositional formula to be returned, instead of “yes.” Among function problems, we are particularly interested in counting problems, in which the answer is the number of solutions to a function problem. The counting analog of SAT is #SAT, which asks the number of satisfying assignments of a propositional formula.

Function problems have their complexity classes. A function problem is in FNP if there is a polynomial-time, deterministic algorithm that, given x and y, checks whether y is a possible output for x. For counting problems, the analog of FNP is the #P class. If a decision problem is hard, the corresponding counting problem is also hard—because knowing the number of solutions means also knowing whether there are solutions. The converse is not true. There are easy decision problems that give rise to hard counting problems. For example, 2SAT is in P, but #2SAT is #P-complete.

Fix a decision problem, say, SAT. Checking whether a SAT instance has a unique solution is at least as hard as checking whether it has at least one solution: if we know that the instance has exactly one solution, we also know that it has at least one. Checking whether a SAT instance has exactly one solution is no harder than counting its solutions: if we have counted the solutions, we know whether their number is 1.

To make things more “interesting,” though, the problem we are concerned with—whether a puzzle has a unique solution—is not exactly any of the prob-lems discussed so far. Why? Because the question we want to answer is whether, given that a puzzle has a solution, it also has another one.

Why does the knowledge that there is a solution affect the difficulty of check-ing whether there is another solution? Consider graph coloring, which is NP-complete when the number of colors is at least 3. Suppose, however, that we have computed one k-coloring of a graph. Then, we can cheaply obtain k! − 1 other k-colorings by permuting the colors.

So, a way to put the question of uniqueness is this: For puzzle type X, given a solution to a specific puzzle, is there a cheap way to determine whether there is another solution for the same puzzle that is applicable to all puzzles of type X? (X could be Slitherlink, for example.) Since our preferred method of checking for additional solutions involves calling the SAT solver again, it doesn’t seem that we believe that such a cheap way exists for our two puzzle types. In fact, we don’t (unless P = NP). In the remainder of this section, we provide justification for our belief.

First, let’s give a name to the problem we want to discuss. For a puzzle type P (e.g., Slitherlink) we denote by ASP P the problem of deciding whether, given an instance of P (e.g., a Slitherlink puzzle) and a solution to that instance, there exists another solution.11 (ASP stands for Another Solution Problem [11]). ASP P, as we defined it, is a decision problem, which, for both Sloop and Slitherlink, has been proved NP-complete.

For some problems P, there are direct proofs that ASP P is NP-complete. As in the practice of NP-completeness, though, once a problem ASP P' is known to be NP-complete, we can try to reduce it to another problem ASP P to prove the latter is NP-complete. The key ingredient of such an approach is a parsimonious reduction, that is, a reduction that provides a bijection between the solutions to the two problems. This way, if we have an instance of P' and a solution to it, we can map those to an instance of P and one of its solutions. If we find that the instance of P has no other solution, since the solutions of the two problems are in one-to-one correspondence, we know that the instance of P' does not have another solution either. We need both the reduction from P' to P and the mapping from the solutions of P' to the solutions of P to be computable in polynomial time. Then, we can argue that, if we had a polynomial algorithm to solve ASP P, we would have a polynomial algorithm to solve ASP P'.

Parsimonious reductions have been used to prove that counting problems are #P-complete. Their role in the ASP context underlies the connection be-tween these problems. The good news for those who work with another-solution problems is that many reductions used to prove NP-completeness results are parsimonious. Based on parsimonious reductions, Yato [13] has introduced the notion of ASP-complete problem and proved that Slitherlink is ASP-complete. If P is ASP-complete, counting its solutions is #P-complete and its decision version is NP-complete. Problems related to Slitherlink that have been proved ASP-complete include the Hamiltonian circuit problem for undirected graphs with maximum degree 3 [8] and for grid graphs with maximum degree 3 [7].

7 The Project

The goal of this project is to implement two Z3-based solvers: one for Sloop and one for Slitherlink. The experience you gain with the Sloop solver will help you tackle the Slitherlink solver. Each solver consists of five files. A “starter kit” is available on Canvas. It contains, for each puzzle type:

• A file (sloopinputs.py for Sloop and slilininputs.py for Slitherlink) containing a function called get_grid that takes an integer i as input and returns the i-th puzzle from a predefined collection. A Sloop puzzle is just a sequence of sequences of integers, where 1 represents a black square, and 0 represents an empty cell. In a Slitherlink puzzle, each entry of the sequence of sequences is either None (no clue) or an integer between 0 and 4 (a clue). This file also contains a function called check_grid to check the integrity of a puzzle grid. Finally, it contains a function called parse_command, which reads the command line.

• A file (sloopdisplay.py for Sloop and slilindisplay.py for Slitherlink) containing implementations of the Unicode and matplotlib-based display functions. The implementations are complete except for the Slitherlink matplotlib-based function.

• A file (sloopverify.py for Sloop and slilinverify.py for Slitherlink) that contains a function called verify that takes a grid and a purported solution and checks whether the latter is indeed a solution to the puzzle de-scribed by the former. Your code must call this function for each solution it finds. The function has an optional Boolean parameter (allow_weak) that makes it skip the check for a single loop.

• A file (sloop.py for Sloop and slilin.py for Slitherlink) containing a skeleton of the solver. This file is where most of your implementation work will take place. In particular, you will have to define variables, add constraints to the solver, and implement the solve_and_print function.

• A file (slooprun.py for Sloop and slilinrun.py for Slitherlink) to run your solver on all provided puzzles in one batch and collect the results in one file. The file has various options to control the experiment. Use the -h option to find out.

The two solvers should take arguments from the command line that specify the following:

• -p n to request solution of the n-th puzzle (from the collection in the “inputs” file). The first puzzle is number 0.

• -m to request matplotlib output instead of Unicode.

• -d to request that the solver draw the unsolved puzzle (in the format determined by the -m switch) and quit.

• -a to request that the displayed solution include also the values of the p variables. (See Figure 4.) This option is only required to take effect when the -m option is also specified.

• -s n to request that at most n solutions be computed. By default, the solver should find all solutions and report their count.

• -v to control the amount of output produced by the solver. This option may be repeated (-v -v or -vv) to increase the verbosity of your program. It is up to you to decide what gets printed at each verbosity level. You should use to make the debugging of your programs more convenient.

• -h to cause the solver to print a short help message.

The parsing of the options and the (automated) generation of the help message is already available through parse_command. The functionality requested with those switches, of course, needs to be implemented.

8 Implementation Issues

Throughout this section, we assume that the solver object is referenced through a Python variable named slv.

8.1 Interacting with the Z3 Solver Object

Since all Z3 variables are Boolean in both our puzzle types, slv = SolverFor (’QF_FD’) is the recommended choice.

When the solver has determined that the constraints are satisfiable, we can access the satisfying assignment by the model() method of the Solver class. We have to be careful, though, because Z3 may assign no value to certain variables. The event is pretty rare because, for a variable not to receive a value, there must be two equally valid solutions that only differ in the value of that variable. We still need to do something about it. Fortunately, Z3 can be asked to do model completion. Suppose you inquire the value of the Boolean variable x that did not get a value during the satisfiability check. Then slv.model()[x] returns None. Calling slv.model().eval(x), however, returns x. Finally,

slv . model () . eval (x , model_completion = True )

will cause Z3 to add an arbitrary value for x to the model and return it. This is exactly what we want. It also leaves the model in the right state for when we later add a blocking clause to count the number of solutions. This approach is al ready implemented (for both puzzles) in the provided function evaluate_model.

If, for whatever reason, slv.check() returns unknown, a call to

slv . reason_unknown ()

will return an explanation string, which can be printed. It may be a little cryptic, but it’s usually better than nothing.

Finally, it may be convenient to call simplify on constraints before adding them to the solver. The simplification only applies simple rules. (See Figure 9 for a sample of what it can and cannot do.) However, if you call print(slv), perhaps to check whether the constraints you’ve added are the ones you meant, the simplified forms may be easier to read.

8.2 Visualizing the Solution

The ability to visualize the solutions to the puzzles is important, not only for the finished program, but also for the early “drafts.” Images like the ones of Figure 6 are reasonably easy to understand. Good luck, however, interpreting the output of print(slv.model()) without significant extra work. It’s safe to say that carefully planning the visualization of the puzzle solutions is key to the success of your project.

Python has a powerful visualization library that some of you may have al-ready used: matplotlib. Matplotlib does not ship with the standard Python distribution, but it can be installed easily. With its help one can draw the puzzle as given, the solved puzzle, or the puzzle with the values of the p variables. The code for the first two tasks is provided to you.

It is also possible to print a solution to the terminal window in which the program is running. In this case, you may want to use Unicode box-drawing

And (True , a) -> a

And (False , a) -> False

And ( And (a , b) , c) -> And (a , b , c)

Or (a ) -> a

And () -> True

Or () -> False

Not ( Not ( a)) -> a

Or (a , a ) -> a

And (a , Not ( a)) -> False

If (a , b , b ) -> b

If (a , True , False ) -> a

If (a , False , True ) -> Not ( a)

Implies (a , a) -> True

Implies ( Not (a) , a) -> a

Xor (a , Not ( a)) -> True

a == True -> a

(a == a ) == b -> b

And ( Or (a ,b) , Not ( Or (b ,a))) -> False

PbEq ((( a ,1) ,(b ,1) ,(c ,1) ) ,0) -> Not ( Or (a , b , c))

AtLeast (a , b , c , 1) -> Or (a , b , c )

AtLeast (a , b , c , 3) -> And (a , b , c)

AtMost ((a , b , c) , 1) -> AtLeast ( Not (a) , Not (b ) , Not (c) ,2)

PbEq ((( a ,1) ,(b ,1) ,(c ,1) ) ,1) -> PbEq ((( a ,1) ,(b ,1) ,(c ,1) ) ,1)

a == (a == b) -> a == (a == b )

And (a , Or (a , b) ) -> And (a , Or (a , b) )

And (a , Or ( Not (a) , b) ) -> And (a , Or (b , Not (a )))

And ( Or (a ,b) , Or (a , Not (b))) -> And ( Or (a ,b ) , Or (a , Not (b )))

Figure 9: Examples of results produced by simplify. Z3 applies a combination of constant propagation, rewriting in standard form, and simple heuristics. The last few lines of the table above show that simplify does not really do Boolean reasoning. Hence, it does not realize that And(a,Or(a,b)) is equivalent to a. Of course, these limitations only apply to simplify. If we ask Z3 whether the constraint And(a,Or(a,b))!= a is satisfiable, the answer is “no.” characters to produce output that is easier to read than plain “ASCII art.” This “low-budget” solution makes it easy to run a batch of puzzles, while saving the solutions in one file.

In other respects, the Unicode solution is less satisfactory. On the one hand, a path traced with box-drawing characters is usually more difficult to follow than one traced with real graphics. On the other hand, adding the values of the p variables to a diagram made with box-drawing characters turns it into a mess.

In case you are wondering, the puzzle figures in this document were generated by the solvers in LATEX format, using the TikZ package. This type of output is not required in your project: while the quality is the highest, you would need to install LATEX and learn how to use it. Feel free to inquire if you are interested.

8.3 Debugging Your Project

Even before you run your program, you should consider using Python’s typing hints in your code so that a type checker for Python like mypy may detect some problems. Programs annotated with type hints are easier to read, especially when you return to them after a hiatus. The annotations take some time to enter, but they also help you to answer the question, “What did I have in mind when I wrote this?”

Most Python programming environments provide a symbolic debugger—for example, an interface to pbd, the Python debugger— which allows you to step through the execution of your program, set breakpoints, and inspect variables. You may want to know how to run that debugger, even though you may not use it often.

Finally, for any program of reasonable complexity, the author(s) should plan how to make debugging easier from the beginning. We already discussed the importance of good visualization of the solution in Section 8.2. It is also a good idea to have an easy way (e.g., from the command line) to control the amount of detail printed by your program. In standard mode, your program should only print the solution and the time taken, but when requested to be more verbose, it should report on whatever else you think may help you with the debugging. This is what the -v option of parse_command is for.

When debugging small examples, it may make sense to print the constraints added to the solver. This can be done in two ways. The simpler is

print ( slv )

The limitation of this approach is that, if there are many constraints—or asser-tions, as they are called in Z3—it will not print all of them: at some point, it will print three dots (i.e., an ellipsis) and give up. So, if you want to see all the contents of the solver, you need to iterate through the assertions yourself. For example:

for assertion in slv . assertions () :

print ( assertion )

8.4 Gathering Statistics

The Solver class has a statistics() member function that will report various quantities describing the behavior. of the solver. Not all those quantities are meaningful to someone without detailed knowledge of Z3’s functioning. How-ever, you will quickly realize that a long run involves many decisions and back-jumps, among other things.

The CPU time reported by print(slv.statistics()) is the time taken by the last call to the check() method, not the cumulative CPU time spent by the solver. Besides, a significant fraction of the CPU time is spent in communicating the constraints to the solver. Therefore, it is a good idea to measure the CPU time spent by your program from start to finish. Python’s time package supplies all the necessary functions. Their use is illustrated by the skeleton solvers that you download as part of the Starter Kit.