# How it solves

I use Minisat to solve the puzzle. I associate a variable with each edge - boolean for whether or not it's in a loop. There is a constraint for each vertex (the count of the edges connected to the vertex, and in a loop, must be either 0 or 2), and for each number (the count of the edges surrounding the number, and in a loop, must equal the number).

The above doesn't rule out multiple loops as a solution. I can't think of a practical way to specify that constraint in Minisat, so instead I check each Minisat solution and figure out if there's a slitherlinks solution in it.

The above also doesn't rule out zero loops. I could also check that with each Minisat solution, but instead I add a constraint at the beginning that rules out any Minisat solution with no loops.

If there are multiple slitherlinks solutions, instead of stopping at the first one, I keep going until hitting UNSATISFIABLE. Minisat+ has an option to ask for all the solutions, but with Minisat you need to negate each solution, add that as a constraint, and continue solving. Instead of negating the entire solution, if there is more than one loop, I negate each loop individually. More on that below.

I limit the number of runs of the solver, and the number of slitherlinks solutions. I don't think that's going to get in the way of reasonable puzzles, but I know there are unreasonable puzzles that can hang up the solver without those limits. (Try "3x3:i")

The algorithm:

• For each Minisat solution:
• Break it into separate loops.
• Count the number of loops that abut at least one number.
• If there is exactly one:
• If there are more than one:
• None of them is a slitherlinks solution.
• If there are none:
• Each of the loops, none of which abuts a number, is a solution.
• Negate each of the loops, add those contraints, and solve again.