This is a demonstration of using the minisat SAT solver to solve slitherlink puzzles in your web browser. I generated a javascript version of minisat by using emscripten, which compiles any language that LLVM likes into javascript's ASM. They claim that the result can run at near-native speed. My experience is consistent with that.

Let me repeat that in case it went by too quickly. The puzzle is not being solved by a server somewhere. The solver is written in javascript, and running in your browser.

A note on browsers: I've run this successfully on chrome and safari (including an iphone).
This does **not** run on firefox. I don't want to spend the time right now figuring out what's wrong.
Everybody should have chrome at least for an emergency backup browser, right?

Enter a puzzle by one of the following methods...

- Click one of the example buttons.
- Type into the textarea below the puzzle area, or copy and paste into the textarea.
- Enter the constraints for a square by clicking in a square in the puzzle area, then selecting 0-3 or none. If you're using this method you may occasionally need to use the "Clear" button. Plus you may need to change the number of rows and columns.

Rows:

Columns:

<-- Explained
below

You can type a puzzle into the textarea below, or copy and paste. Use a period for squares that have no constraint. I remove all whitespace. There's an example below the textarea for you to copy and paste.

.01.1.0.33.2.2.12. 1...2..3..2..0...2 ...1.2......2.3... .2.2..3.03.3..3.1. 2..0.1.1..2.2.1..1 2..3.2.1..1.1.2..1 .3.2..2.11.3..0.1. ...1.2......1.2... 3...1..1..3..2...3 .02.1.3.10.3.0.10.

After you solve a puzzle, you can click the "Next" button and it will check for another solution. It displays it if there is one. Otherwise it says "unsolvable". A proper slitherlink puzzle has only one solution, but an underconstrained one has more.

Here's a fun thing to do: Set the rows and columns to 2x2, then, without adding any constraints on the squares, click "Solve" then repeatedly click "Next". You can see all thirteen solutions.

If you're interested in how long it takes to solve a puzzle, so you can compare it to other methods of solving, then to be fair you need the "Next" button to find out how long it takes to exhaust all possibilities. Minisat uses heuristics in its search for a solution, so it may find a solution to a difficult problem very quickly by luck. So you need to hit "Next" to finish the search.

I needed to do that to make sure I wasn't just lucky when my solver solved example 3 so quickly. Example 3 is the testcase named C95 in this paper. The authors of the paper tried using various solvers on C95. The main topic of their paper is a ZDD method, and it couldn't finish C95 (presumably ran out of memory). They tried a Sugar plus SAT solver method, and it took over 1000 seconds. I'm guessing that was due to a combination of (1) improvements in computer speed in the handful of years since they did this, (2) improvements in SAT solvers, and (3) Sugar was trying to do pre-optimizations that used more time than they saved. Actually, (3) isn't a guess. I ran experiments with Sugar and minisat and it spent way too much time in Sugar. Anyway, the point of all this is I had to make sure I was making a fair comparison before deciding my solver was significantly faster.

They did mention a faster solver, one specifically written for slitherlink puzzles. (Sadly, I couldn't find it online. The link had gone cold.) But, really, how many times do you want to keep solving individual NP-Hard problems before you start putting your energy into a universal solution? (i.e., a SAT solver)

Comments to doug[at]DougAndJean[dot]com