Sudoku, also known as "Number Place," is a logic game especially popular in Japan but gaining popularity throughout the world. The game is played on a square 9 by 9 grid, split up into 9 square 3 by 3 "sections".The goal of the game is to complete the grid so that each number appears exactly once in each row, column, and region. Further constraints are provided by "givens," fixed numbers that must remain unchanged in the grid.
Below is a sample grid:
For more information on the game:
Determine how to "compile" a Sudoku problem into clausal form propositional logic. Implement such a compiler in a language of your choice, and solve the test problems using the SAT solvers WalkSat (a local search solver) and zChaff (a backtracking solver).
To make the problem more interesting, you must solve sudoku problems of varying size, not simply the classic 9x9 with 3x3 regions. In the general n^2 by n^2 sudoku problem, the grid is n^2 by n^2 and contains n^2 regions of size n by n. Instead of using the numbers 1-9, the generalized problem uses numbers 1-n^2. In all games, each number must appear exactly once in each row, column, and region.
To give a concrete example, n=3 is the classic sudoku game, n=3. For n=4, the task is to fill a 16 by 16 grid with the numbers 1 to 16, such that no row, column, or 4 by 4 region has the same number twice. For n=1, there exists only one possible game solution.
Sudoku type problems become harder to solve if some of the clues are erased. (In general this causes the puzzle to have more than one correct solution.) Our test suite includes problems with various percentages of the clues erased. Take timing measurements as WalkSat and zChaff solve your encodings of these problems. At what sparseness ratio do the hardest problems occur?
Your program must input and output board description files in the following format:
You are free to make the problem size (n) a command line parameter. We provide you with 50 example problems in each of 3 sizes, at 5 levels of sparsity, along with solutions: sudoku_examples.zip.
Filenames in sudoku_examples.zip can be interpreted as follows:
[problem size]_[sparsity]_[index].[problem or solution]
Problem size:
Sparsity:
Index ranges from 000 to 050, corresponding to the 50 distinct problems at each size.
Files ending in .sol are solutions to the erase00 files. (More sparse versions may have multiple solutions. If multiple solutions exist, your solver should still find one of them.)