I’ve been working on my sudoku solver.
It’s not the most efficient sudoku solver, by a long way. But the goal is not really just to solve sudoku. It’s to solve sudoku using pure logic, and to be able to show a logical path to the solution. If I wanted to just solve sudoku, I’d implement DLX.
The basic principles are quite simple. The problem is expressed in terms of logical statements constructed as disjunctions of predicates, where a predicate takes the form of “Box (X,Y) contains Z”, or “Box (X, Y) does not contain Z”.
There is essentially one logical deduction rule used. Two statements are resolved to produce one or more new statements by finding a eliminating complementary terms and joining up the result with an OR. For example, “(8,7) isn’t 5 or (8,8) isn’t 5” can be resolved with “(8,8) is 5” to produce “(8,7) isn’t 5”.
There is a constraint on the knowledge base which is that no statement can be equal to, or be a subset of, any other statement.
For (some kind of) efficiency, statements with a smaller number of terms are looked at first. Looking at a term involves resolving it with all other statements with which it can be resolved.
This converges pretty quickly for simple sudoku grids, but can take much longer for hard ones. So far I’ve tried it on some of the hardest “unsolvable” puzzles I’ve been able to find on the Internet, and while it does take a very long time for those (over an hour for some puzzles) it does eventually converge and give a correct result.
Perhaps one of the more interesting aspects of a solution using this method is that the solver can construct a DAG of the entire proof. The downside of this is that I now have to figure out a way of actually presenting that DAG in a simple enough way that it can be understood by a human. Some sort of pattern matching on the graph to remove “obvious” steps could be one way to go.
For kicks, I tried constructing a dot file from the DAG generated by solving a relatively simple sudoku puzzle, and passing it through dot. The result is an unpleasantly large 110 megabyte postscript file, spanning 285 pages.
I’m looking forward to finding some way to express the proofs more intuitively.