.. _solving-slitherlink:

Solving the Slitherlink Problem
===============================

In this section, we describe an incremental SAT-based solving approach (implemented in function :ref:`solve_slitherlink <slither-solve>`) for the Slitherlink problem. We use the encoding described in the previous section to obtain a solution to the CNF formula generated in line~3 that guarantees that for each cell exactly the amount of edges described by the number associated with the cell are selected and they form a continuous path.

.. _slither-solve:

.. code:: python
    :number-lines:

    def solve_slitherlink(instance, seed, remove_unconstr_subcycles):
        sl = SlitherLink(instance)
        cnf = encode_slitherlink(sl)
        s = Cadical()
        s.set("seed", seed)
        s.add_clauses(cnf.clauses)
        while s.solve() is True:
            # The removal of unconstrained subcycles
            # (i.e. those that do not have any number)
            # is optional, as there might be too many of them.
            n_cycles = sl.manage_subcycles(s, cnf, remove_unconstr_subcycles)
            if n_cycles == 1:
                sl.visualize(s.model(), cnf)
                print("s YES", flush=True)
                return cnf.decode_dimacs(s.model())
        print("s NO", flush=True)


Lines 4 and 5 instantiate the Cadical SAT solver and initialize it with a seed for the random number generator of the solver, and in line 6 we add to the solver the clauses generated by function *encode_slitherlink*. Then, we iteratively query the SAT solver (line 7) to provide a solution (a model). 

In line 11, we call function :ref:`manage_subcycles <slither-cycles>` (which is part of the *SlitherLink* class) that checks the solution reported by the SAT solver. If there is more than one cycle it adds to the SAT solver the clauses that forbid these cycles in the solution. To find the cycles it uses the function *find_cycles*. To discard a cycle just adds to the SAT solver as a clause the negation of all the edges that conform to the cycle.

We also parameterize an option to remove the *unconstrained* cycles (those cycles that do not have any number), as there might be too many of them. On the other hand, it could be beneficial for the SAT solver to remove them. We will analyze this more in depth in the :ref:`Tuning Slitherlink <tuning-slitherlink>` section.

.. _slither-cycles:

.. code:: python
    :number-lines:

    def manage_subcycles(self, solver, cnf, remove_unconstr_subcycles):
        model = solver.model()
        constr_cycles, unconstr_cycles = self.find_cycles(cnf.decode_dimacs(model))
        if len(constr_cycles) > 1:
            cycles = constr_cycles + unconstr_cycles if remove_unconstr_subcycles else constr_cycles
            for subcycle in cycles:
                negate_subcycle = [Not(edge) for edge in subcycle]
                solver.add_clause(cnf.to_dimacs(negate_subcycle))
        return len(constr_cycles)


Then, if only one cycle was found we are done and we have found a solution. We return the solution once decoded the model provided by the SAT solver (line 16). Otherwise, we will exit the main loop (line 7) if there is not a solution with just one cycle and we report the problem has no solution.

The full code for the *find_cycles* method (also part of the *SlitherLink* class) is shown below:

.. code:: python
    :number-lines:

    def unpack_edge(self, line):
        _, i, j, dir = line.name.split("_")
        return int(i), int(j), dir

    def find_cycles(self, model):
        activated = [edge for edge in model if not isinstance(edge, Not)]
        activated_map = {e.name: i for i, e in enumerate(activated)}
        seen = set()
        cycles = []
        for i, init_edge in enumerate(activated):
            if i in seen:
                continue
            cycle = []
            cycles.append(cycle)
            edge = init_edge
            seen.add(i)
            while edge is not None:
                assert not isinstance(edge, int)
                cycle.append(edge)
                j, edge = self.find_next_activated(edge, activated_map, seen)
                if j is not None:
                    seen.add(j)

        constr_cycle, unconstr_cycle = [], []
        for cycle in cycles:
            if self.is_constr_cycle(cycle):
                constr_cycle.append(cycle)
            else:
                unconstr_cycle.append(cycle)
        return constr_cycle, unconstr_cycle

    def satisfies_cell(self, cycle):
        for edge in cycle:
            for i, j in self.get_nearby_cells(edge):
                if self.cells[j][i] is not None:
                    return True
        return False

    def get_nearby_cells(self, edge):
        i, j, dir = self.unpack_edge(edge)
        delta_i, delta_j = (0, 1) if dir == "right" else (1, 0)
        cells = []
        if i < self.m and j < self.n:
            cells += [(i, j)]
        if 0 < i and 0 < j:
            cells += [(i - delta_i, j - delta_j)]
        return cells

    def find_next_activated(self, edge, activated_map, seen):
        for continues in self.get_continuation(edge):
            j = activated_map.get(continues.name, None)
            if j is None or j in seen:
                continue
            return j, continues
        return None, None

    def get_continuation(self, edge):
        i, j, _ = self.unpack_edge(edge)
        ci, cj = self.get_pointing_coordinate(edge)
        return self.vertex_edges(i, j) + self.vertex_edges(ci, cj)

    def get_pointing_coordinate(self, edge):
        i, j, dir = self.unpack_edge(edge)
        delta_i, delta_j = (1, 0) if dir == "right" else (0, 1)
        return i + delta_i, j + delta_j


Analyzing Inconsistent Subproblems
----------------------------------

In other solving strategies, the SAT solver can be used to check whether a partial assignment can be extended to a complete solution to the problem. This is the case for large problems solved through Large Neighborhood Search :cite:p:`lns` techniques where we heuristically identify promising subproblems (neighbourhoods) and solve them *completely*, for example, with a SAT solver. If the subproblem is satisfiable we are done, if it is not, we can retrieve from the SAT solver the reason for this unsatisfiability which is referred to as the unsatisfiable core.  

To define the subproblem we call the SAT solver on a set of assumptions that encode decisions on the edges. If there is no solution we can query the SAT solver about the core of unsatisfiability, i.e., a subset of assumptions that makes the problem unsatisfiable, as shown in :ref:`the following example <unsat-core>`.

.. _unsat-core:

.. code:: python

    (...)
    assumptions = cnf.to_dimacs(fixed_edges)
    if not s.solve(assumptions):
        return cnf.decode_dimacs(s.core())
    (...)


Equipped with the core, now we can decide which decisions in the core should be revoked. This can be done automatically or even with human support, depending on the application.