dMv (daemonv) wrote,
dMv
daemonv

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.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded 

  • 2 comments