July 19, 2012

In addition to our work with the SAT visualization, we have been interested in modeling real problems as Boolean satisfiability problems, particularly Sudoku puzzles. I have been working on a script that takes as input a Sudoku puzzle represented as a string (a sequence of each square's value, from top-to-bottom and left-to-right), converts it to its representation in conjunctive normal form,  and outputs a CNF file readable by MiniSAT.

When represented as SAT problems, Sudoku puzzles are very large (729 literals), but not overly difficult to model.
Sudoku puzzles in SAT require clauses specifying that:
-Every square may only hold values from 1-9, and each square may only hold one value.
-Every value must exist in every row, but must exist only once in each row.
-Every value must exist in every column, but must exist only once in each column.
-Every value must exist in each 3x3 square, but each value may only appear once in that square.
-Each square holding a value at the beginning of the puzzle must be asserted.

There is a fairly elegant literal encoding for Sudoku that makes it much easier to interpret the results of the SAT solver. A square in Sudoku can be represented as p(i, j, n), where i is the row, j is the column, and n is the value assigned to that square. Thus, the clause 234 asserts that the square in the 2nd row and the 3rd column is assigned the value 4. Negation works similarly; -235 asserts that 5 cannot be assigned to the previous square.

I am looking forward to seeing how MiniSAT handles these SAT instances and discovering what can be learned from testing our system on a real problem.

-Maggie