Modelling the Slitherlink Problem
In the Slitherlink problem, we are given an \(n \times m\) grid. A cell in the grid can be empty or contain a number between 0 and 3. Each cell has 4 associated edges (its borders). The goal is to select a set of edges among all cells such that:
If a cell has a number \(k\), then \(k\) of its edges have to be selected.
The selected edges form exactly one cycle that does not cross itself.
Slitherlink input example

Solution example

In this figure we can see an example of the Slitherlink problem and its only correct solution.
The following code snippet shows the source code needed to model into SAT an instance of the problem. First, we generate an instance of the class Problem (line 3). Then, we encode the constraints of the problem. Lines 512 encode the vertex constraints that ensure that the path traced by the solution is contiguous. Line 8 calls the method vertex_edges
, that returns a list of Bool
objects representing edges that intersect at the vertex $i,j$. Lines 912 encode the constraint for the edges of a vertex. A selected edge can be contiguous without crossing iff the number of selected edges that intersect at each vertex is 0 or 2.
Lines 1519 encode the cell constraint for each cell with a number. Line 18 calls the method cell_edges
, which returns a list of Bool
objects representing the edges that surround a cell. Line 19 adds the constraint to the Problem instance.
Then, we encode the problem to CNF DIMACS (line 21) applying the Tseitin transformation [Tse83] and return the underlying CNF object.
def encode_slitherlink(sl):
p = Problem()
# Vertex Constraints
for i in range(sl.m + 1):
for j in range(sl.n + 1):
edges = sl.vertex_edges(i, j)
p.add_constr(
(Add(edges) == 0) 
(Add(edges) == 2)
)
# Cell Constraints
for j, row in enumerate(sl.cells):
for i, cell in enumerate(row):
if cell == None: continue
edges = sl.cell_edges(i, j)
p.add_constr(Add(edges) == cell)
return p.to_cnf_dimacs()
Notice that this model is not taking into account the fact that there has to be exactly one cycle.