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:

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

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