In the first part of this homework, we learn to use SAT solvers to solve some problems. You are asked to write two small programs, encoder and decoder, which can be run on the linux machines.
The problem considered in this homework is the Sudoku Puzzles (classic)
Your encoder will read a 9x9 matrix of integers (0 denotes unknown elements) and then generate a set of propositional clauses in DIMACS CNF format. You then use one of SAT solvers to find a model of the propositional clauses. You also need to write a small program which reads the model and displays the solution of the puzzle.
SAT solvers can be found at www.satlive.org. You may also use my SAT solver ~hzhang/sato/sato on any departmental linux machine. The source code of sato3.2.tgz can be found here.
All of these solvers accept DIMACS CNF format and run on linux systems. Suppose sato is the solver and puzzle_file is the problem file, a linux script would be like
./encoder sudoku1 > sudoku1.cnf ~hzhang/sato/sato sudoku1.cnf > sato_output ./decoder sato_output
where decoder will extract the model from sato_output, decode the model into a solution of the sudoku puzzle, and print out the solution. You need to test your code on other Sudoku files.
Here are the encoder and decoder C files for Einstein Puzzle: encoder.c decoder.c
The second part of the homework will learn to use Prolog as a programming language on Problems 9.13 and 9.14 on Page 317 of our textbook.
On CS linux machines, SWI-prolog is installed (the command is pl). Please see http://www.swi-prolog.org/ and SWI-Prolog Reference Manual. Your code should run in pl.
Hantao Zhang