Problem Set 3: Sokuko Solver

## Overview

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.

## Learning Objectives

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

## Getting Started

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 .

## Problem Description

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)

## A though experiment

As an exercise in explanation we will use the following FiniteSet description. The actual problem will use a more complicated representation.
```grid0 = universe (expand [4,4]) (\ xs -> True)
```
Which looks like this.
```*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
```
Now we can write three functions with type: Int -> Relation -> Relation.
```rowSquares  i grid = ...
colSquares  j grid = ...
```
and which behave as follows:

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

## Representing the actual board

The actual board is more complicated than the board of the thought experiment above. Each square can take on one of 4 possible values, rather than the present, not-present distinction in the thought experiment board. The key to the soduko solver board representation is to use a 3D relation. If the tuple (row,column,digit) is present then digit is present in the square (row,column). Note that more than one digit can be present in a square at the same time. The solution is to constrain the problem so that only one digit appears in any one square.

## What to do

• 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:
```*FiniteSetExamples> row 0 grid
0=p1 \/ p5 \/ p9 \/ p13
1=p2 \/ p6 \/ p10 \/ p14
2=p3 \/ p7 \/ p11 \/ p15
3=p4 \/ p8 \/ p12 \/ p16

0=p1 \/ p5 \/ p17 \/ p21
1=p2 \/ p6 \/ p18 \/ p22
2=p3 \/ p7 \/ p19 \/ p23
3=p4 \/ p8 \/ p20 \/ p24
```
The way to interpret 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.
1. Each digit appears in every row, column, and quadrant.
2. 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.

## Extra Credit

Try one of the following for ectra credit.

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

## What To Turn In

• 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