The solver in Python language uses the PySAT toolkit to solve the sudoku using formulas in the Conjunctive Normal Form (CNF) of Boolean Logic.
The sudoku is divided into nine large quadrants referenced with rows and columns from 1 to 3. Each quadrant contains nine small squares, identified by rows and columns numbered from 1 to 3.
The program takes as input a file with strings in the format "sudoku_i_j_p_q_N", where:
- N is the value (from 1 to 9) that will fill the small square;
- i is the row value of the position of N on the quadrant;
- j is the column value of the position of N on the quadrant;
- p is the row value of the quadrant;
- q is the column value of the quadrant.
The following example shows the input for the "world's most difficult Sudoku" designed by Arto Inkala.
sudoku_1_3_1_1_5
sudoku_2_1_1_1_8
sudoku_3_2_1_1_7
sudoku_1_1_1_2_3
sudoku_3_2_1_2_1
sudoku_2_2_1_3_2
sudoku_3_1_1_3_5
sudoku_1_1_2_1_4
sudoku_2_2_2_1_1
sudoku_3_3_2_1_3
sudoku_1_3_2_2_5
sudoku_2_2_2_2_7
sudoku_3_1_2_2_2
sudoku_1_1_2_3_3
sudoku_2_3_2_3_6
sudoku_3_2_2_3_8
sudoku_1_2_3_1_6
sudoku_2_3_3_1_4
sudoku_1_1_3_2_5
sudoku_3_3_3_2_9
sudoku_1_3_3_3_9
sudoku_2_2_3_3_3
sudoku_3_1_3_3_7
| 1 | 2 | 3 | ||||||||
| 1 | 2 | 3 | 1 | 2 | 3 | 1 | 2 | 3 | ||
| 1 | 1 | 5 | 3 | |||||||
| 2 | 8 | 2 | ||||||||
| 3 | 7 | 1 | 5 | |||||||
| 2 | 1 | 4 | 5 | 3 | ||||||
| 2 | 1 | 7 | 6 | |||||||
| 3 | 3 | 2 | 8 | |||||||
| 3 | 1 | 6 | 5 | 9 | ||||||
| 2 | 4 | 3 | ||||||||
| 3 | 9 | 7 | ||||||||