Slitherlink Solver
Overview
This Slitherlink solver translates a puzzle into a SAT ("boolean satisfiability") problem, which is then solved by a SAT solver. The translation is done here; the SAT solver was obtained here. This is a brute force method that is guaranteed to solve all puzzles that have a solution. (The solver was tested on a batch of 93,000 puzzles, including 7000 20x14's, and solved 100%.) More...There is one wrinkle: a Slitherlink puzzle cannot be completely translated into a SAT problem. It's not possible (or at best not practical) to translate the rule that the solution must consist of a single loop only. So the SAT solver will most often find a series of solutions to the SAT problem that imply two or more loops, and for each such (false) solution more constraints are added to the SAT problem until a solution is found that implies only one loop. At that point it's an easy matter to look for an additional solution to the puzzle by adding a constraint that rules out the specific solution that was found, and this can be repeated until all solutions have been found. (However, it is standard for a Slitherlink puzzle to have only one solution.)
This solver would not have been written if it weren't for this Slitherlink solver, which also uses SAT and solves all puzzles. Prior to discovering that site I had no knowledge of SAT. This solver was written from scratch and takes a different approach to translating a puzzle. That solver is (much) faster than this one, but the difference only becomes apparent with very large puzzles or puzzles that have many solutions.
The example puzzle was generated at this site.
Usage Notes
When a puzzle is solved, the solution is immediately displayed, then the solver looks for an additional solution. If it finds one, the 'Next' button is displayed. When the 'Next' button is clicked, the additional solution that was found is displayed, then the solver looks for another solution, etc. The 'Solve' button will be disabled when, and only when, the solver is executing. Clicking 'All' will get up to 50 solutions. Right-click 'Prev' to return to the first solution. After getting all solutions, right-clicking 'Next' is equivalent to clicking 'Prev'.
With the cursor in the puzzle code input, press: Tab to solve the puzzle, Enter to draw the puzzle, Shift-Enter to convert to/from an expanded puzzle code.
A puzzle can be edited by clicking on the squares. The puzzle code will be updated with each click. Right-click to set a square to the same value as the last square edited. To create a new puzzle, type WxH (W=Width, H=Height, e.g., 10x10) for the puzzle code and press Enter.
A puzzle code can be passed as a parameter in the URL:
The puzzle will be solved when it loads, unless "nosolve" is added as a parameter (pc=4x4:33a2a213g3&nosolve).
Click the heading ('SAT Slitherlink Solver') to add the current puzzle code to the URL with the 'nosolve' parameter. If the current puzzle code is already in the URL, inclusion of the 'nosolve' parameter will be toggled. Right-click the heading to remove a puzzle code from the URL.
Performance is dependent on the device and brower, of course, but generally speaking the solver is fast. But when the puzzles get very big, performance does degrade. A 50x50 puzzle might take more than 30 seconds. So, to avoid the messiness of having to kill processes, the solver will time out at 1 minute. When looking for an additional solution it will time out at 10 seconds. Open the Developers Console (F12) before execution starts to see activity while the solver is executing.
Puzzle Code
A "puzzle code" is in the form: WxH:S, where W and H are integers indicating the width and height of the board (in squares), and S is a string of characters that indicates where the numbers are placed on the board, from left to right and top to bottom. A lower case letter is used to indicate one or more blank squares: a = 1, b = 2, etc.
For example, the code for the following puzzle is 4x3:b2230d1a
| 2 | 2 | ||
| 3 | 0 | ||
| 1 |
A puzzle can also be defined (here and at the other SAT Slitherlink solver site) by an "expanded puzzle code," which uses one character for each square, with rows separated by line feeds, or any whitespace character at this site.
For example, the puzzle above can be entered as:
..22 30.. ..1.
At this site, a minus sign or underscore can be used for blank squares instead of a period.