A rather grand name for programs which combine and manipulate logic clauses in order to produce more logic clauses is
theorem provers. Hopefully, there will be eventually enough logic statements to prove or refute some assertion. A
theorem proving program looks appropriate for the
computer game version of
Sudoku.
Sudoku is about placing the numbers from one to nine inclusive on a 9x9 matrix. The numbers in every row, column or 3x3 subblock must be all different. (Several variations exist, but will not be discussed here.)
The first way to proceed is to discount all numbers occuring in the same row, column or subblock as some square. Hopefully, only one candidate number will be left. More useful, if not as obvious, perhaps, is to find eight squares in a subblock which cannot hold a certain number- then it must go to the ninth. The next technique is considering
pairs, but this page is more about theorem provers than sudoku and will not go that far. Still, typically two out of three puzzles are solved completely. The partial solution can be passed to another method which cannot fail, such as
backtracking.
Timing of millisecond programs is not a task at which the site is proficient, but the compiled version solves the puzzle given about 650 times per second on the 1.8 GHz Celeron. As it probably takes a minute to enter puzzle data into a file, this looks adequate.
Of course, all puzzles do not need the same number of sweeps- some will even accept multiple solutions. (These may not be considered genuine sudoku puzzles by the purists.)
It is obvious to you that a square cannot hold two numbers, but it is not 'obvious' to the computer, which must be supplied with the corresponding production rule. Were you to use a general theorem prover, and letters instead of numbers, you might well have to explain to it that 'A' is a different leter from 'B'. A theorem proving program tends to produce a lot of correct, but irrelevant, logic statements.
Here is the
program for this section (
improved version- 70% success). It uses arrays to store the number in every square, as well as the numbers which
cannot be held in the square. While these clearly are not independent, it is very convenient to have both.
For my own code up to this point: Valid XHTML 1.0!