January 27th, 2006
|05:21 pm - Solving Sudoku|
One of the nice things about where my office is located is the conversations I overhear. Yesterday, Bob Harper and Stephen Brookes were having an animated discussion on something (not unusual). But wait, they're talking about... yes... solving Sudoku. Ed Clarke walks by, and they interrogate him: Could you solve sudoku problems with a SAT checker?
His feeling was that yes, you probably could.
Sudoku is a very simple and well-known puzzle that has achieved international popularity in the recent past. This paper addresses the problem of encoding Sudoku puzzles into conjunctive normal form (CNF), and subsequently solving them using polynomial-time propositional satisfiability (SAT) inference techniques. We introduce two straightforward SAT encodings for Sudoku: the minimal encoding and the extended encoding. The minimal encoding suffices to characterize Sudoku puzzles, whereas the extended encoding adds redundant clauses to the minimal encoding. Experimental results demonstrate that, for thousands of very hard puzzles, inference techniques struggle to solve these puzzles when using the minimal encoding. However, using the extended encoding, unit propagation is able to solve about half of our set of puzzles. Nonetheless, for some puzzles more sophisticated inference techniques are required.I. Lynce and J. Ouaknine, Sudoku as a SAT Problem, 9th International Symposium on Artificial Intelligence and Mathematics, January 2006.
While I was in the Caymans this year, I tried my first Sudoku problem. Both of my aunts are ...
fans players solvers addicts ... brought books down. I tried my first Sudoku problem and didn't like it. I thought I probably should like it. I think I like the notion, and I think I like the thought of playing them as people do -- a casual wake-up on the train ride to work, or a way to unwind the mind after a busy day. I feel like this for crossword puzzles, too, but I am no good at them. This is patterns, numbers, I should feel comfortable.
Part of what is interesting about Sudoku, as a cultural phenomenon, is how it separates those who approach it. If you are a programmer, you can not avoid thinking about writing some code. Which is crazy, because it is an obviously solvable problem of no consequence. You take on a sudoku for the glory of what? The pleasure of sitting down and letting your logical brain do some work. If you can't write the brute force version, you are not a programmer. If you can't write a backtracking solver, or some thing of that nature, that says something. Looking at Sudoku as a SAT problem does not tell us anything new about people like Harper. My approach, because I didn't have access to the Wikipedia article on the Math of Sudoku was to try to figure out the *size* of the space. I wasted a couple of cycles on my mother's iBook in that pursuit (there are only 6.7×1021 boards), but then, I'm a number junkie.
I leave it as an open question whether it is a waste of one's time to spend time teaching a computer to solve a time wasting exercise. The best augmented Sudoku site I've encountered is Squobble, a basic flash interface that provides you with tile counts and correctness checks and nothing more. There are some nice interactive solvers if you want to learn strategies.
|Date:||January 28th, 2006 12:53 am (UTC)|| |
I like sudoku. I found them in the london times when I was in france last year, and I didn't put down the paper until I finished them (well, except for some meetings I had to have). A breadth-first search is how I solve them in my mind, so a computer has got to be able to do that pretty trivially.
|Date:||January 28th, 2006 02:12 am (UTC)|| |
If you like sudoku puzzles but wish that they involved more math, check out some kakuro puzzles. I haven't found a good website that presents online versions well, but they are worth checking out.