Sudoku and the way of the SAT solver

Oct 07, 2009 19:35

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 ( Read more... )

Leave a comment

bramcohen October 9 2009, 12:37:56 UTC
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.

Non-consecutive Sudoku can be trivially built using the obvious clauses. The ballooning isn't a big deal, or at least, is far less than the ballooning necessary to do the basic encoding of sudoku in the first place.

Target sum sudoku can be expressed by having cells for additive values. For example, there's a cell for all values of A + B, with clauses containing 3 elements essentially making a lookup table for sums, then another one for A + B + C with another set of clauses doing the same thing for the adding up the A + B cells and the C cell, and so on for everything making up a single sum constraint. Such constraints are by their nature quite loose and can easily result in high runtimes.

For cases where dancing links can represent the problem straightforwardly it will generally do better than a general SAT solver, because it's doing the same logic with some implementation tricks which make it faster. It's sort of in the same vein though, in that dancing links supports generalized constraints, just not as generalized as full-blown CNF. (That's Conjunctive Normal Form, which is the type of constraint I describe in the post.)

Your comments about which problems take longer to solve I think correspond accurately with the innate difficulty of those problems, so different techniques will generally give similar relative performance times.

Reply


Leave a comment

Up