September 6, 2005
SAT & Sudoku
It seems SAT has been used once again … just for fun!!!
For those who do not know the SATisfiability problem, which is a very well-known Computer Science problem, might imagine it simply as the problem of finding if a formula has a solution and if there is at least one solution you should find one, we call it a model. SAT works tradicionally on propositional (boolean) formulas but it is not required to be that way.
Anyway, it seems someone decided it is time to finish off the publishing of those god damn books which come with dozens of sudoku problems… why solve a sudoku problem if we can solve a problem that solves the sudoku problem? And that problem is SAT… Check it and play with it… it’s fun… and if have just by chance a SAT solver try it… you have never though your SAT solver could solve Sudoku, right???
(in theory… it can solve mostly anything… I believe I’m saying “mostly” because I can’t really understand how it would be possible to safe Portugal from a huge financial hole… even with a SAT solver at hand!)