Sudoku and the way of the SAT solver

[bramcohen]

Writing a Sudoku solver is a slightly tricky but reasonably straightforward problem. Here I'll present a non-obvious way of implementing it which is short in terms of lines of code and also much easier to modify and extend than the more direct approaches. The general technique is applicable to a very wide range of problems, so hopefully someone

Comments

[gregstoll]

Very cool! When I wrote my Clue solver, I tried reducing it to a SAT problem, but eventually had to give up and use Clue-specific logic because it took forever. I was just using a textbook algorithm, so it's possible using a "real" solver would have helped a lot...

[misterajc]

OK, so now I had to compare your code with my sudoku solver. (I had to write one, as I was spending far too much time solving them manually.) I took twice as many lines (in perl) to write a sudoku specific solver, but mine had a user interface and comments. You win on elegance, but I actually used mine to cure a sudoku addiction.

[bramcohen]

I worked on the blackbox solver, eons ago, before constraint solvers were even a general category, and came up with walksat for it. Constraint solvers have come a long way since then though, I keep meaning to read up on how survey propagation works but haven't waded through it yet.

[bramcohen]

I wrote a custom SAT solver in this case just to show the technique. It is of course more practical to just use a general one.

TMTOWTDI

[knowbuddy]

I teach an Advanced Database Structures course for a Bachelors program. Our review for the mid-term exam is to write a Sudoku solver in SQL. It's a great review, as it ends up using unions, several types of joins, aggregate functions, and most of the base concepts they'll need for the second half of the course. I get everyone up at the white board and we figure out, together, how to solve the generic case, then variations.

It turns out that you need 4 or 5 tables and as many (very simple) queries to populate them with data. Once you've done that, it's just a repetition of two queries to iteratively solve the puzzle.

The students always have fun with it, even though they are disappointed to see how easy it is.

[onigame]

I've not investigated SAT solvers much, but some of the things I would worry about as regards to generalizing to other types of Sudoku puzzles would be

[bramcohen]

Udoku can be represented straightforwardly. The clauses saying that a digit must appear in each cell remain, but the clauses which say that a digit must occur at least once in each row and column go away. They're redundant anyhow, but speed things up a lot, hence the udoku solver running slower