KR: Exercise 1a

Propositional Satisfiability (SAT)

Introduction

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:

1. Black (removed) cells cannot be horizontally or vertically adjacent
2. 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 at
http://www.hitoriconquest.com/?puzzleSize=5

Steps

We will build a program that performs the following steps:

1. 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:
   
   
   

   11214 15543 14132 25335 42511

   
   
2. 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)
   

   
   
3. Call the solver picosat. Read picosat's output and recognize the obtained model (if one is found).
   
   
4. 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 black cell:
   
   

   *12*4 15*43 *4132 2*3*5 4251*

   
   

Additional comments

• For simplicity, we can assume that the number of rows and columns coincide (square grids of n x n, where n >=0)
• 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
• hitori1.txt, solution1.txt (the example shown above)
  
• hitori2.txt (a 2x2 square with no solution)
  
• hitori3.txt, solution3.txt
• hitori4.txt, solution4.txt
  

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 prácticas.