26 Jul
2005
26 Jul
'05
9:10 p.m.
"Gary" == Gary McGuire <Gary.McGuire@nuim.ie> writes:
Gary> If you want a hard sudoku try (omitted): Gary> I believe that this one cannot be solved without trial and error Gary> (aka guesswork). It can be. I wrote a small python program to translate sudoku puzzles into DIMACS CNF (conjunctive normal form) used by a lot of SAT solvers. There is a preprocessor called hypre by Fahiem Bacchus which just uses something called "Hyper resolution" -- a limited form of deduction (which it turns out the CNF that I generated is ideal for). So far, the preprocessor -- which makes no guesses -- has solved every sudoku I've thrown at it, including your challenge above (and in much less than 1 second). Victor