Solving the Slitherlink Problem

In this section, we describe an incremental SAT-based solving approach (implemented in function solve_slitherlink) 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.

def solve_slitherlink(instance, seed):
    sl = SlitherLink(instance)
    cnf = encode_slitherlink(sl)
    s = Cadical()
    s.set('seed', seed)
    s.add_clauses(cnf.clauses)
    while s.solve() is True:
        n_cycles = sl.manage_cycles(
        s, cnf)
        if n_cycles > 1: continue
        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 8, we call function manage_cycles 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.

def manage_cycles(self, solver, cnf):
    model = solver.model()
    cycles = self.find_cycles(
        cnf.decode_dimacs(model)
    )
    if len(cycles) > 1:
        for cycle in cycles:
        clause = [~edge for edge in cycle]
        solver.add_clause(
            cnf.to_dimacs(clause)
        )
    return len(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 12). 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.

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 [PR10] 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 the following example.

(...)
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.