SuViSa
About SuViSa
SuViSa is a Sudoku-puzzle solver, by converting a Sudoku instance into a SAT (Wikipedia page on SAT) instance and feeding that to a SAT-solver. The result of the SAT-solver is then read in and converted back to the Sudoku puzzle.
This program is not intended as the ultimate Sudoku solver, although provided a fast SAT-solver is used it will be reasonably fast. The reason I wrote this program is that I realised that the way to solve Sudoku puzzles quickly resembles the way a SAT-solver works. I wanted to prove that one could use a SAT-solver as a Sudoku solver, and that it would result in a very small program that could be written quickly (I did it in under two hours).
To use this program, you also need a SAT-solver (not included in the package). Known fast SAT-solvers can be found through the pages of the SAT-solver competition (http://www.satcompetition.org). The SAT-solver has to comply with the rules for input and output specified by the SAT-competition.
The program should be compilable on most Un*x variants, although I've only tested it on Linux. To compile, type make (or gmake if your default make doesn't work and you do have GNU make installed).
NOTE: I do not offer support for this program, as it is only a proof-of-concept program. If you can provide me with a patch to make it work on a particular flavour of Un*x, I will integrate the patch. You can reach me by e-mail on suvisa <at> ghalkes.nl.
The input format of the program is very simple. Lines starting with a '#' character are ignored (comments). The rest of the input should consist of a list of numbers, the first two of which denote the horizontal and vertical size of the small blocks in the Sudoku puzzle. All other numbers are either 0 for a square that must be computed, or a number from 1 to the maximum number to be used for a square with a given number. You can use newlines wherever you want. See problem[1236].sdk for examples. The size of the problem is limited only by the amount of free disk space (for storing the SAT instance) and the limits of the SAT-solver.
To run SuViSa type
SuViSa <SAT-solver> <puzzle>
with <SAT-solver> replaced with the exact path of the SAT-solver, and <puzzle> replaced with the exact path of the puzzle-instance file.
Theory
To convert the puzzle into a SAT instance, I split the Sudoku rules into the following rules:
each row must contain each number once
each column must contain each number once
each block must contain each number once
each square in the puzzle can contain only one number
For each square I create a binary variable for each possible value denoting whether or not that value is written in this square. This is also the reason why we need rule 4. Now each rule can be simply rewritten into a set of clauses by noting that we can write the condition "one and only one of x variables must be true" in conjugate normal form (CNF) as:
(a V b V c V ... V x) ^ (-a V -b) ^ (-a V -c) ^ ... (-a V -x) ^ (-b V -c) ^ (-b V -d) ^ ... ^ (-b V -x) ^ ... ^ (-w V -x)
In other words: the first clause denotes that at least one must be true, and all the combinations of two variables both in negated form denote that no more than one must be true.
For each number, for each row/column/block we can create such a set of clauses. This will encode rules 1 through 3. Rule 4 can be encoded by using the same set of clauses but using all the number variables for a single square. This of course has to be done for all squares in the original puzzle.
Last, but not least, the given numbers have to be encoded by adding clauses consisting of a single variable, i.e. the variable corresponding to that number in that square.
You can have a look at the produced SAT instance by running SuViSa with -s as the SAT-solver. The file will be named outXXXXXX with the X's replaced by some random characters. The name to which the instance has been saved will also be printed on screen.
Download
The source for SuViSa 1.0 can be downloaded here.
Copyright Notice
Copyright © 2005 G.P. Halkes
SuViSa is distributed under the Academic Free License version 2.0.
