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 = ...
quadSquares k 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
*FiniteSetExamples> quad 0 grid
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.
- 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.
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
- Be prepared to talk about your solution in class.
Back to the class web-page.
Back to the Course Schedule.