SudokuSolver < Main

r3 - 17 Feb 2010 - 15:06:05 - SatoshiKonnoYou are here: TWiki >

Sudoku Solver

Sudoku is a major number placement puzzle in Japan, and it can be encoded as a SAT problem [1]. According to the paper, I wrote simple scripts to solve the problem using SAT solver. To download the scripts and samples, please check attachment files of this page smile

CNF Encoding for Sudoku Problem

Variables

Each cell of Sudoku needs nine variables to encode into CNF format, I map the variables as the following. The number of variables are 729.

11[1-9]	12[1-9]	13[1-9]	14[1-9]	15[1-9]	16[1-9]	17[1-9]	18[1-9]	19[1-9]
21[1-9]	22[1-9]	23[1-9]	24[1-9]	25[1-9]	26[1-9]	27[1-9]	28[1-9]	29[1-9]
31[1-9]	32[1-9]	33[1-9]	34[1-9]	35[1-9]	36[1-9]	37[1-9]	38[1-9]	39[1-9]
41[1-9]	42[1-9]	43[1-9]	44[1-9]	45[1-9]	46[1-9]	47[1-9]	48[1-9]	49[1-9]
51[1-9]	52[1-9]	53[1-9]	54[1-9]	55[1-9]	56[1-9]	57[1-9]	58[1-9]	59[1-9]
61[1-9]	62[1-9]	63[1-9]	64[1-9]	65[1-9]	66[1-9]	67[1-9]	68[1-9]	69[1-9]
71[1-9]	72[1-9]	73[1-9]	74[1-9]	75[1-9]	76[1-9]	77[1-9]	78[1-9]	79[1-9]
81[1-9]	82[1-9]	83[1-9]	84[1-9]	85[1-9]	86[1-9]	87[1-9]	88[1-9]	89[1-9]
91[1-9]	92[1-9]	93[1-9]	94[1-9]	95[1-9]	96[1-9]	97[1-9]	98[1-9]	99[1-9]

Rules

Sudoku is consist of the following four rules.

SR1	Each cell contains an integer in the range 1 to 9
SR2	No two cells in any row contain the same value
SR3	No two cells in any column contain the same value
SR4	No two cells in any separated 3x3 block contain the same value

The rules are encoded as the following CNFs.

SR1	(111 or 112 or ... or 118 or 119) and ... and (991 or 992 or ... or 998 or 999)
SR2	((111 or 121) and (111 or 131) ... and (171 or 191) and (181 or 191)) and .... ((919 or 929) and (919 or 939) ... and (979 or 999) and (989 or 999))
SR3	((111 or 211) and (111 or 311) ... and (711 or 911) and (811 or 911)) and .... ((199 or 299) and (199 or 398) ... and (799 or 999) and (899 or 999))
SR4	((111 or 121) and (111 or 131) ... and (171 or 191) and (181 or 191)) and .... ((779 or 789) and (779 or 799) ... and (979 or 999) and (989 or 999))

Running the program

Using the above variables and rules, I wrote simple scripts to generate CNF format for the specified problem of Sudoku. To use the scripts, please check the following command log. To solve the CNF format, I used MiniSAT.

$ less sudoku-problem.in
0 0 3 0 0 4 0 2 0
0 0 6 0 0 0 0 0 9
8 0 0 0 1 0 0 0 0
0 0 5 0 0 0 0 9 0
0 7 0 0 0 3 0 1 0
0 4 0 0 0 5 6 0 0
0 0 0 0 8 0 0 0 1
3 0 0 0 0 0 4 0 0
0 1 0 6 0 0 5 0 0

$ python sudoku-sat-gen.py < sudoku-problem.in > sudoku-problem.cnf

$ MiniSat_v1.14_linux sudoku-problem-01.cnf sudoku-problem.ans

$ python sudoku-sat-out.py < sudoku-problem.ans >sudoku-problem.out

$ less sudoku-problem.out
7 5 3 8 9 4 1 2 6
1 2 6 3 5 7 8 4 9
8 9 4 2 1 6 3 5 7
2 3 5 1 6 8 7 9 4
6 7 8 9 4 3 2 1 5
9 4 1 7 2 5 6 8 3
5 6 7 4 8 2 9 3 1
3 8 9 5 7 1 4 6 2
4 1 2 6 3 9 5 7 8

Notes

1. Lynce and J. Ouaknine: SUDOKU as a SAT Problem, 9th International Symposium on Artificial Intelligence and Mathematics, January 2006.

Topic attachments
I	Attachment	Action	Size	Date	Who
ans	sudoku-problem.ans	manage	4.7 K	16 Feb 2010 - 15:15	SatoshiKonno
cnf	sudoku-problem.cnf	manage	106.4 K	16 Feb 2010 - 15:14	SatoshiKonno
in	sudoku-problem.in	manage	0.2 K	16 Feb 2010 - 15:14	SatoshiKonno
out	sudoku-problem.out	manage	0.2 K	16 Feb 2010 - 15:15	SatoshiKonno
txt	sudoku-sat-gen.py.txt	manage	1.2 K	16 Feb 2010 - 15:13	SatoshiKonno
txt	sudoku-sat-out.py.txt	manage	0.3 K	16 Feb 2010 - 15:14	SatoshiKonno

Main