adrianwilker / sudoku-solver

Sudoku solver using the PySAT toolkit.

sudoku-solver

👨‍💻 About it

The solver in Python language uses the PySAT toolkit to solve the sudoku using formulas in the Conjunctive Normal Form (CNF) of Boolean Logic.

⚙ How it works

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