Sudoku Solver using SAT Solver for Structural Complexity Course.
Normalize the input, assign sat structures for the current unknown variables.
X 2 X X X X X X X
X X X 6 X X X X 3
X 7 4 X 8 X X X X
X X X X X 3 X X 2
X 8 X X 4 X X 1 X
6 X X 5 X X X X X
X X X X 1 X 7 8 X
5 X X X X 9 X X X
X X X X X X X 4 X
Output will resolve (satisfy) the current sudoku matrix if formula is satisfiable.
[ 1 | 2 | 6 ][ 4 | 3 | 7 ][ 9 | 5 | 8 ]
[ 8 | 9 | 5 ][ 6 | 2 | 1 ][ 4 | 7 | 3 ]
[ 3 | 7 | 4 ][ 9 | 8 | 5 ][ 1 | 2 | 6 ]
[ 4 | 5 | 7 ][ 1 | 9 | 3 ][ 8 | 6 | 2 ]
[ 9 | 8 | 3 ][ 2 | 4 | 6 ][ 5 | 1 | 7 ]
[ 6 | 1 | 2 ][ 5 | 7 | 8 ][ 3 | 9 | 4 ]
[ 2 | 6 | 9 ][ 3 | 1 | 4 ][ 7 | 8 | 5 ]
[ 5 | 4 | 8 ][ 7 | 6 | 9 ][ 2 | 3 | 1 ]
[ 7 | 3 | 1 ][ 8 | 5 | 2 ][ 6 | 4 | 9 ]
Inspired by RogerGuTeng's SudokuSolver written in Java & other solutions written in python.