In this assignment you will use the knowledge you gained in exercise 4 and exercise 5 that dealt with finite sets and use of the MiniSat solver to build a Sodoku solver.

- Incorporate your CNF transformation from Problem 2 into a module you can import into this problem and the Minisat library.
- Learn to combine the skills of using the FiniteSet library and the MiniSat solver to create solutions to constraint based problems.
- Learn to extract properties from FiniteSets using the operators one, some, none, full, subset, and functional dependency.
- Use the Minisat.hs library to create *.cnf files and to script calling the MiniSat program from inside of a Haskell program.

You will need to take a few preliminary steps before you get started.

- Read the notes on finite sets. Pay particular attention to the examples (especially the 8-queens example) and the section on Scripting Minisat.
- If you haven't already done so, down load the FiniteSet library and the Prop and put them in your code directory.
- You will also need to download the new file Minisat library described in the notes.
- You will also need your solution to Problem 2 which implements
the CNF library and exports the function
**toCNF**. This library is imported by the Minisat library, which uses the function**toCNF**. You may also need to call**toCNF**in the solution to this assignment, so be sure it is in your code directory. Be sure your solution conforms to the template CNF.hs that was given in the Problem 2 description. It is important that module be named "**CNF**" and that the function that converts to CNF be called "**toCNF**". -
**Pointing the Minisat library at your version of MiniSat solver.**In order to script the use of MiniSat solver, the Minisat library must know where it lives on your machine. Open your version of Minisat.hs, near the top is a line that looks like:minisat = "D:\\cygwin\\usr\\local\\bin\\minisat.exe"

This line declares a variable (of type String) that points to the executable for the MiniSat solver tool. Put a string here that is the full path to your working copy of the solver. Be sure that the path is in the appropriate style for your machine. Since my machine is a windows machine, the path has back-slashes between directories. I must double the backslash to make it appear in the string. Once you have done this test it by loading only Minisat.hs and typing:

solveWithMinisat "test.cnf" "test.sol" [LetterP 2]

If MiniSat starts up, you have succeeded in pointing the scripting tools to the executable. Here are some hints on installing MiniSat on windows .

Your goal is to write a solver for a 4-by-4 soduko solver, which is a smaller version of the traditional 9-by-9 problems found in news papers, magazines, and puzzle books. A problem of size 4-by-4 consists of a grid with 4 rows and 4 columns and 4 quadrants. The goal is to fill in the grid such that each square contains one of the digits 1, 2, 3, or 4. The rules require that every row, every column, and every quadrant contain 4 different digits. A picture of such a grid, with some of the squares are filled in looks like this.

It is a good metaphor to address each square with a pair (row number,column number), as follows.

(0,0) | (0,1) | (0,2) | (0,3) |

(1,0) | (1,1) | (1,2) | (1,3) |

(2,0) | (2,1) | (2,2) | (2,3) |

(3,0) | (3,1) | (3,2) | (3,3) |

grid0 = universe (expand [4,4]) (\ xs -> True)

*FiniteSetExamples> grid0 (0,0)=True (0,1)=True (0,2)=True (0,3)=True (1,0)=True (1,1)=True (1,2)=True (1,3)=True (2,0)=True (2,1)=True (2,2)=True (2,3)=True (3,0)=True (3,1)=True (3,2)=True (3,3)=True

rowSquares i grid = ... colSquares j grid = ... quadSquares k grid = ...

quadSquares 1 grid0 = (0,2)=True (0,3)=True (1,2)=True (1,3)=True |
quadSquares 0 grid0 = (0,0)=True (0,1)=True (1,0)=True (1,1)=True |
rowSquares 3 grid0 = (3,0)=True (3,1)=True (3,2)=True (3,3)=True |
colSquares 2 grid0 = (0,2)=True (1,2)=True (2,2)=True (3,2)=True |

I.e. each function computes a subset of the squares from the grid. The rowSqures picks out a row, colSquares picks out a column, and quadSquares picks out a quadrant.

- Define grid as a 3D (4-by-4-by-4) relation. Associate a differnt
propositional letter with each triple. Hint: use the functions
**enum**and**count**. See the notes for example uses. The first few tuples look like this*FiniteSetExamples> grid (0,0,0)=p1 (0,0,1)=p2 (0,0,2)=p3 ... (3,3,2)=p63 (3,3,3)=p64

- Define
**rows**,**cols**, and**quads**functions which are 3D relation to 1D relation functions. These are similar to but different from the thought experiment functions rowSquares, colSquares, quadSquares. Here are some sample outputs:The way to interpret*FiniteSetExamples> row 0 grid 0=p1 \/ p5 \/ p9 \/ p13 1=p2 \/ p6 \/ p10 \/ p14 2=p3 \/ p7 \/ p11 \/ p15 3=p4 \/ p8 \/ p12 \/ p16 *FiniteSetExamples> quad 0 grid 0=p1 \/ p5 \/ p17 \/ p21 1=p2 \/ p6 \/ p18 \/ p22 2=p3 \/ p7 \/ p19 \/ p23 3=p4 \/ p8 \/ p20 \/ p24

**row 0 grid**is row zero has a 0 if**(p1 \/ p5 \/ p17 \/ p21)**is true. Note that there is nothing to stop row zero from having more that one digit under some valuations of the propositional letters. Hint: Use**select**and**project**on grid. - Define constraints on grid by using the operators
**one**,**some**,**none**,**full**,**subset**, and**funDep**.- Each digit appears in every row, column, and quadrant.
- Each square has exactly one digit. (hint: use funDep).

- Extract a list of formulae describing the constraints.
- Use the function
**solveWithMinisat**from the**Minisat**module to get a solution. - Apply the solution to grid, and show that the instantiated
grid is indeed a soltuion.

- Find more solutions for a given problem where some of the squares have been assigned concrete digits.
- Find solutions for 9-by-9 puzzle. If this takes a long time discover where the bottle neck in the proble is.

- Be sure your name is listed as a comment
in your solution, you have named your solution
P2.hs - Drop it in the ProbSet3 folder in the class drop box
- Be prepared to talk about your solution in class.