A Sudoku solver with a custom DPLL decision procedure.
./sudoku_z3_api.py <path_to_grid_file>
./sudoku_z3_smtlib2.py <path_to_grid_file>
./sudoku_dpll.py <path_to_grid_file>
./sudoku_z3_api.py
: Solver using Z3 API (slow)./sudoku_z3_smtlib2.py
: Solver writting an SMTlib2 file and parsing the output of z3 (fast)./sudoku_dpll.py
: Solver with an embedded DPLL solver written by myself (very fast and not using z3)
Each line represents a value in the initial grid:
- (i, j, value) were i, j and value are intergers in 1 .. 9
Three grid are available in the directory tests/
to test the different solvers:
test_sat
: solvable gridtest_unsat
: unsolvable gridtest_hardest
: very difficult grid made by Arto Inkala and taken from https://www.telegraph.co.uk/news/science/science-news/9359579/Worlds-hardest-sudoku-can-you-crack-it.html
- Solvable grid (0 represents a missing value):
Initial grid:
|2|9|0|3|0|8|0|0|0|
|0|0|6|4|0|0|0|5|0|
|0|0|0|7|0|0|0|9|0|
|0|0|1|0|0|0|0|0|8|
|7|0|0|0|9|0|3|0|0|
|3|0|0|0|0|0|0|0|5|
|0|0|0|0|0|2|0|0|6|
|0|8|0|0|1|0|5|0|0|
|5|2|0|0|8|0|0|0|0|
Solved grid:
|2|9|4|3|5|8|1|6|7|
|1|7|6|4|2|9|8|5|3|
|8|3|5|7|6|1|2|9|4|
|9|5|1|2|4|3|6|7|8|
|7|6|2|8|9|5|3|4|1|
|3|4|8|1|7|6|9|2|5|
|4|1|9|5|3|2|7|8|6|
|6|8|7|9|1|4|5|3|2|
|5|2|3|6|8|7|4|1|9|
- Unsolvable grid (0 represents a missing value):
Initial grid:
|2|2|0|3|0|8|0|0|0|
|0|0|6|4|0|0|0|5|0|
|0|0|0|7|0|0|0|9|0|
|0|0|1|0|0|0|0|0|8|
|7|0|0|0|9|0|3|0|0|
|3|0|0|0|0|0|0|0|5|
|0|0|0|0|0|2|0|0|6|
|0|8|0|0|1|0|5|0|0|
|5|2|0|0|8|0|0|0|0|
Grid unsolvable!