.. _modelling-slitherlink:

Modelling the Slitherlink Problem
=================================

In the Slitherlink problem, we are given an :math:`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 :math:`k`, then :math:`k` of its edges have to be selected.
* The selected edges form exactly one cycle that does not cross itself.

.. _fig-slither:

+-----------------------------+-----------------------------+
| | |slither1|                | | |slither2|                |
| | Slitherlink input example | | Solution example          |
+-----------------------------+-----------------------------+

.. |slither1| image:: ../../images/slitherlink01.png
   :alt: Slitherlink input example
   :align: middle

.. |slither2| image:: ../../images/slitherlink03.png
   :alt: Slitherlink example solved
   :align: middle


In :ref:`this figure <fig-slither>` we can see an example of the Slitherlink problem and its only correct solution.

To model and solve the Slitherlink problem we will use the following Python class (we will add more methods later when we need them):

.. code:: python
    :number-lines:

    class SlitherLink:
        def __init__(self, path):
            with open(path) as f:
                self.cells = [
                    [None if char in ["-", "."] else int(char) for char in line.strip()]
                    for line in f
                ]
            self.n = len(self.cells)
            self.m = len(self.cells[0])

        def edge(self, i, j, dir):
            # We represent each edge using a boolean variable where:
            #   - (i, j) is the position of its "top-left" vertex of the edge
            #   - "dir" is the direction of the edge
            return Bool(f"Edge_{i}_{j}_{dir}")

        def vertex_edges(self, i, j):
            intersection = []
            if i > 0:
                intersection += [self.edge(i - 1, j, "right")]
            if j > 0:
                intersection += [self.edge(i, j - 1, "down")]
            if i < self.m:
                intersection += [self.edge(i, j, "right")]
            if j < self.n:
                intersection += [self.edge(i, j, "down")]
            return intersection

        def cell_edges(self, i, j):
            return [
                self.edge(a, b, dir)
                for a, b, dir in [
                    (i, j, "right"),
                    (i, j, "down"),
                    (i + 1, j, "down"),
                    (i, j + 1, "right"),
                ]
            ]

The following :ref:`code snippet <slither-enc>` 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 5-12 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 9-12 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 15-19 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 :cite:p:`Tseitin1983` and return the underlying CNF object.

.. _slither-enc:

.. code:: python
    :number-lines:

    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 is 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.