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 grid
• test_unsat: unsolvable grid
• test_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!