Task 1 (8 points): Naive Constraint Solving
• Implement the naive constraint solving algorithm in the AIMA book (Chapter 6,
Section 6.3, Page 215, Figure 6.5; it is the same as shown in slide 47 from
class), by filling in the missing parts of the given ‘sudoku.py’ file. Feel free make
minor changes to the given code, but the data structure should stay roughly the
same.
The naive algorithm should solve the easy puzzles quickly. It can take several minutes
to solve the hard ones this way.
Task 2 (8 points): Use More Pruning
• Extend the code with more advanced solving techniques as explained in this
post. Create a new solver class and don’t overwrite the solver from Task 1. Note
that the techniques are closer to the set-based pruning that we discussed in
class, tailored to solving Sudoku. Clearly, you can not just copy paste their code,
but need to understand it and then adapt it without changing the data structure
The advanced algorithm should now solve the hard puzzles quickly.
Task 3 (8 points): Translate to SAT to Solve
• Implement an encoding of Sudoku as propositional logic formulas in conjunctive
normal forms, and use a state-of-the-art SAT solver to solve. Read
the notes.pdf file for more details. The hard1.cnf file in the cnf directory is
the encoding of the first hard instance in the code. You need to generate the CNF
files, pass them to a SAT solver (see below) to solve, and then parse the output
from the SAT solver and plug them back into the original problem and display the
solutions. If you don’t have time to finish the whole thing but generate the right
CNF files, you can earn 5 points.
SAT Solvers to Use
I recommend PicoSAT as the default choice. Go to its webpage, download, and compile
(simply do ./configure.sh and then make). The binary picosat can then take the
CNF files you produce (always use extension .cnf).
I highly recommend that you find a linux/mac machine to use the solver. If you have to
use windows, this note may be helpful but I haven’t tried. If you have difficulty in getting
PicoSAT to work, try cryptominisat which has more instructions about making things
work on windows.
If you want to know about more solvers, check the page for the annual SAT solver
competition.
Extra Credits
• (3 Points) Check performance on more benchmarks (these easy ones and
these hard ones). Produce a plot that shows the the performance difference of
the three approaches (with a timeout of 5 minutes or something on the naive
algorithm).
• (5 Points) If you have even more time and interest, scale everything to 16 by 16
problems (right now it is 9 by 9), and generate some problems. Check how the
three appraoches differ in performance.