First things first, using a SAT Solver.

Most modern SAT solvers use the DIMACS input format for a CNF formula. A CNF formula is encoded in DIMACS as follows: (a) variables are represented by natural numbers (1 and above) and (b) negations of variables by the minus sign, (c) each clause is described in a line terminated by a zero.

As an example, the formula

(x1)(x2 x3)(x4 x1)(x1 x2 x3 x4)(x2 x4) would be encoded as:

p cnf 4 5 10 2 -3 0 -4 -1 0 -1 -2 3 4 0 -2 4 0

For this assignment we will use the MiniSat SAT solver, which is one of the fastest SAT solvers currently available (and impressively the smallest code-base wise). You can find the MiniSat solver pre-compiled binaries here.

Given a DIMACS input file, say input.dimacs, you can run MiniSat as follows:./minisat input.dimacs output.txt

where, minisat is the binary for MiniSat and output.txt is an output file where MiniSat will write SAT if the input is satisfiable and UNSAT otherwise. In case of SAT, it also outputs a satisfiable assignment.

You can find sample inputs on blackboard. We strongly encourage you to explore these files and MiniSatbefore starting the assignment.

9. Solve Sudoku with MiniSat. Sudoku is played on an n n board, where n is a perfect square. Some cells are pre-filled with numbers from 1 to n; the rest are blank. The board is subdivided inton n blocks. The goal is to fill each cell with a number in such a way that each number from 1 to n occurs exactly once in each row, each column, and each block. While the usual case is to have a unique solution, we generalize the problem so that multiple solutions are also possible. For example, if no cell is pre-filled, you can fill the cells however you wish as long as the above mentioned constraints are met.

For this problem, you will write a program which does the following:

1. (a) (5 points) read a Sudoku puzzle from an input file (input format described below),

2. (b) (20 points) encode the Sudoku puzzle as a CNF formula in DIMACS format,

3. (c) (10 points) use MiniSat to find a satisfying assignment to the CNF formula,

4. (d) (15 points) read the satisfying assignment produced by MiniSat to generate the solution to the

   original Sukodu problem given as input and output to a file (output format also described below).

In the input file, the first line has just one number n, the size of the puzzle grid, which is guaranteed to be a perfect square. Every other line is a single-space separated list of numbers between 0 and n(inclusive) corresponding to a row of the Sudoku puzzle. A 0 denotes a blank cell. There are n such lines for all the rows. The output format is similar except that the first line specifying n is absent and there are no 0s (as every cell has to be filled).

Here is an example.

Sample Input

Homework Assignment 1 Due: February 14, 2019 at 11:59pm

Sample Output

9 963174258

060104050 008305600 200000001 800407006 006000300 700901004 500000002 007206900 040508070

178325649 254689731 821437596 496852317 735961824 589713462 317246985 642598173

You can use any CNF encoding you want in order to use the SAT solver. Here is a suggested encoding. Let the boolean variable xr,c,d be true iff the number d is in the cell at row r, column c. Encode the following constraints, along with the prefilled cells: - Exactly one number appears in each cell. (Hint : Exactly one is the same as at least one and at most one.)

- Each number appears exactly once in each row. - Each number appears exactly once in each column. - Each number appears exactly once in each block.

Your solver will take five command-line arguments, as follows:

 ./solver InputPuzzle OutputSoln MiniSatExec TempToSat TempFromSat 

where InputPuzzle is the file containing the input puzzle, OutputSoln is the file to which you will out- put the solution, MiniSatExec is the filename of the MiniSAT executable (e.g., MiniSat_v1.14_linux),TempToSat is the name of the temporary DIMACS file that your solver will produce, and TempFromSatis the solution that MiniSAT will generate.

You can write your program in any programming language you desire. You must include README file with instructions to compile and I should not need to install any software.

Some sample 99 inputs are posted on blackboard.