KR: Exercise 1a
Propositional Satisfiability (SAT)
In this exercise we will play with a
propositional satisfiability (SAT) solver to find
solutions to Hitori puzzles. Hitori
is a puzzle that consists in removing (marking as black)
some digits in a grid of cells so that the remaining cells
do not repeat any number in a same row or a same column. A
pair of constraints are applicable:
- Black (removed) cells cannot be horizontally or
- All white cells must be connected altogether: we must
be able to reach any white cell from another by vertical
or horizontal movements through white cells.
To understand the game rules, you can try to play online
We will build a program that performs the following
Read an Hitori puzzle from a text
file with the following format: one text line of n
characters (a digit from 1 to 9) per each Hitori row.
As an example, the file could look like:
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
(¬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
Hitori solution and print the final result in standard
output. The solution will show an '*' in each resulting
- For simplicity, we can assume that the number of rows
and columns coincide (square grids of n x n, where n
- Again, for simplicity, we assume that each cell has a
single digit between 1 and 9. In general, Hitori allows
numbers greater than 9.
- A possible solution for representing that all white
cells are connected can be downloaded here.
- These are some problem instances and their solutions
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 7th, 2014 using the lab work mailbox
or buzón de