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.
1def solve_slitherlink(instance, seed, remove_unconstr_subcycles):
2 sl = SlitherLink(instance)
3 cnf = encode_slitherlink(sl)
4 s = Cadical()
5 s.set("seed", seed)
6 s.add_clauses(cnf.clauses)
7 while s.solve() is True:
8 # The removal of unconstrained subcycles
9 # (i.e. those that do not have any number)
10 # is optional, as there might be too many of them.
11 n_cycles = sl.manage_subcycles(s, cnf, remove_unconstr_subcycles)
12 if n_cycles == 1:
13 sl.visualize(s.model(), cnf)
14 print("s YES", flush=True)
15 return cnf.decode_dimacs(s.model())
16 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 manage_subcycles (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 Tuning Slitherlink section.
1def manage_subcycles(self, solver, cnf, remove_unconstr_subcycles):
2 model = solver.model()
3 constr_cycles, unconstr_cycles = self.find_cycles(cnf.decode_dimacs(model))
4 if len(constr_cycles) > 1:
5 cycles = constr_cycles + unconstr_cycles if remove_unconstr_subcycles else constr_cycles
6 for subcycle in cycles:
7 negate_subcycle = [Not(edge) for edge in subcycle]
8 solver.add_clause(cnf.to_dimacs(negate_subcycle))
9 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:
1def unpack_edge(self, line):
2 _, i, j, dir = line.name.split("_")
3 return int(i), int(j), dir
4
5def find_cycles(self, model):
6 activated = [edge for edge in model if not isinstance(edge, Not)]
7 activated_map = {e.name: i for i, e in enumerate(activated)}
8 seen = set()
9 cycles = []
10 for i, init_edge in enumerate(activated):
11 if i in seen:
12 continue
13 cycle = []
14 cycles.append(cycle)
15 edge = init_edge
16 seen.add(i)
17 while edge is not None:
18 assert not isinstance(edge, int)
19 cycle.append(edge)
20 j, edge = self.find_next_activated(edge, activated_map, seen)
21 if j is not None:
22 seen.add(j)
23
24 constr_cycle, unconstr_cycle = [], []
25 for cycle in cycles:
26 if self.is_constr_cycle(cycle):
27 constr_cycle.append(cycle)
28 else:
29 unconstr_cycle.append(cycle)
30 return constr_cycle, unconstr_cycle
31
32def satisfies_cell(self, cycle):
33 for edge in cycle:
34 for i, j in self.get_nearby_cells(edge):
35 if self.cells[j][i] is not None:
36 return True
37 return False
38
39def get_nearby_cells(self, edge):
40 i, j, dir = self.unpack_edge(edge)
41 delta_i, delta_j = (0, 1) if dir == "right" else (1, 0)
42 cells = []
43 if i < self.m and j < self.n:
44 cells += [(i, j)]
45 if 0 < i and 0 < j:
46 cells += [(i - delta_i, j - delta_j)]
47 return cells
48
49def find_next_activated(self, edge, activated_map, seen):
50 for continues in self.get_continuation(edge):
51 j = activated_map.get(continues.name, None)
52 if j is None or j in seen:
53 continue
54 return j, continues
55 return None, None
56
57def get_continuation(self, edge):
58 i, j, _ = self.unpack_edge(edge)
59 ci, cj = self.get_pointing_coordinate(edge)
60 return self.vertex_edges(i, j) + self.vertex_edges(ci, cj)
61
62def get_pointing_coordinate(self, edge):
63 i, j, dir = self.unpack_edge(edge)
64 delta_i, delta_j = (1, 0) if dir == "right" else (0, 1)
65 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 [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.