Slitherlink, Minisat, and Emscripten

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...

...and then click "Solve".

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.

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