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

[ingulf]

For many problems, it may be easier to use a SMT solver: http://combination.cs.uiowa.edu/smtlib/solvers.html
These are a generalisation of SAT solvers, which have a higher level input
language.

[taral]

Heh. My solver tries to be human-like, but merges a whole bunch of advanced techniques into a 2-SAT reduction.