Sudoku Solver

Usage

  • ./sudoku_z3_api.py <path_to_grid_file>
  • ./sudoku_z3_smtlib2.py <path_to_grid_file>
  • ./sudoku_dpll.py <path_to_grid_file>

Characteristics of Solvers

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

Grid Format

Each line represents a value in the initial grid:

  • (i, j, value) were i, j and value are intergers in 1 .. 9

Test Grids

Three grid are available in the directory tests/ to test the different solvers:

Output Examples

  • 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!
Nicolas Amat
Nicolas Amat
PhD Student in Model Checking

My research interests include model checking, Petri nets and SMT solving.

Related