KR: Exercise 1a
Propositional Satisfiability (SAT)
Introduction
In this exercise we will play with a
propositional satisfiability (SAT) solver to find
solutions to Sudoku puzzles. Sudoku is a popular
puzzle that consists in arranging digits (from 1 to 9) in
a 9 x 9 grid so that no row, column or each of the nine 3
x 3 subgrids contain a repeated digit. For an example, see
the Sudoku
wikipedia entry.
Steps
We will build a program that performs the following steps:
-
Read a sudoku puzzle from a text
file with the following format: one text line of 9
characters per each sudoku row. Any character
different from '1' to '9' is interpreted as an empty
cell. As an example, the file could look like:
53..7....
6..195...
.98....6.
8...6...3
4..8.3..1
7...2...6
.6....28.
...419..5
....8..79
|
-
Find a suitable translation of the
puzzle into a propositional satisfiability problem.
Represent the problem in CNF as a set of clauses, and
generate an auxiliary text file using DIMACS CNF
format. As an example, the following file:
c This is a comment line
c and a second comment line
p cnf 4 3
-1 2 -4 0
1 -2 3 0
2 4 0
|
Lines beginning with "c" are comments. The first
non-comment line begins with a "p" followed by "cnf"
and two numbers: the number of atoms (in the example,
4) and the number of clauses (in the example, 3).
Below, we must include 3 lines, one per clause, and
all ended by "0". Each number is a literal for atoms 1
to 4: if negative, it corresponds to the negation of
an atom. The example above corresponds, therefore, to
the CNF:
(¬p1 \/ p2 \/ ¬p4) /\ (p1
\/ ¬p2 \/ p3) /\ (p2 \/ p4)
- Call the solver picosat.
Read picosat's output and recognize the obtained model
(if one is found).
- Translate back the propositional model into a complete
sudoku and print the final result in standard output.
Assessment & delivery
The maximum grade for this exercise (1a)
is 0,7 points. The deadline for delivery of
exercises 1a and 1b is Friday,
March 1st, 2013 using the lab work mailbox
or buzón de prácticas (further
instructions will be added here).
|