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:
You wouldn't need to do this if Minisat didn't produce multiple-loop solutions. But it's easy to come up with a puzzle that has N places where it can generate M little loops, which means (if you negate the entire solution) M^N calls to the Minisat solver. That's too slow. By negating the individual loops, it breaks the exponential, and makes it fast enough.
It would be cleaner just to count the number of loops, and if there's more than one, it's not a solution. But there can be slitherlinks solutions embedded in a Minisat solution, and you want to detect them as soon as they show up, or you have an exponential problem.
If there are no non-zero constraints, then all the loops in the Minisat solution are, individually, slitherlinks solutions. You could reject the total Minisat solution, and wait for the individual loops to come up by themselves, but that would be slow. Instead I save each one individually as a slitherlinks solution, and reject each one individually to reduce the number of Minisat runs needed.
Back to main slitherlinks page
Comments to doug[at]DougAndJean[dot]com