yices, awk, ocaml を使って秒速で数独を解く

awk yices

yices という SMT Solver を使って、数独を秒速で解いてみた。

http://sourceforge.net/projects/ssyao/
git clone git://git.code.sf.net/p/ssyao/code ssyao-code

数独を解くための制約式を awk （と勉強を兼ねて ocaml ）で作ってやり、yices にその式を解かせる、というもの。

まず yices のインストール。
http://yices.csl.sri.com/
っといってもダウンロードして解凍し、パスを通せば良い。

awk/ocaml へ渡す入力はこんな感じ：

$ cat input_1.txt
11  5
12  3
15  7
21  6
24  1
25  9
26  5
32  9
33  8
38  6
41  8
45  6
49  3
51  4
54  8
56  3
59  1
61  7
65  2
69  6
72  6
77  2
78  8
84  4
85  1
86  9
89  5
95  8
98  7
99  9

この入力は wikipedia のを拝借した。
http://en.wikipedia.org/wiki/Sudoku

これを sudoku_solver.awk に食わせると：

$ awk -f sudoku_solver.awk input_1.txt
(define x11 :: int)
(define x12 :: int)
...
(define x98 :: int)
(define x99 :: int)
(assert
	(and
		(<= 1 x11) (<= x11 9)
		(<= 1 x12) (<= x12 9)
...
		(<= 1 x98) (<= x98 9)
		(<= 1 x99) (<= x99 9)
		(distinct x11 x12 x13 x14 x15 x16 x17 x18 x19)
...
		(distinct x91 x92 x93 x94 x95 x96 x97 x98 x99)
		(distinct x11 x21 x31 x41 x51 x61 x71 x81 x91)
...
		(distinct x19 x29 x39 x49 x59 x69 x79 x89 x99)
		(distinct x11 x12 x13 x21 x22 x23 x31 x32 x33)
...
		(distinct x77 x78 x79 x87 x88 x89 x97 x98 x99)
		(= x11 5)
		(= x12 3)
		(= x15 7)
		(= x21 6)
		(= x24 1)
		(= x25 9)
		(= x26 5)
		(= x32 9)
		(= x33 8)
		(= x38 6)
		(= x41 8)
		(= x45 6)
		(= x49 3)
		(= x51 4)
		(= x54 8)
		(= x56 3)
		(= x59 1)
		(= x61 7)
		(= x65 2)
		(= x69 6)
		(= x72 6)
		(= x77 2)
		(= x78 8)
		(= x84 4)
		(= x85 1)
		(= x86 9)
		(= x89 5)
		(= x95 8)
		(= x98 7)
		(= x99 9)
))
(check)
(show-model)

こんな感じで、yices へ入力する制約式を吐き出す。制約とは、

  • 各マスに入る数字は1?9
  • 行、列に並ぶ数字は重複してはいけない
  • 3x3のマトリックスの中の数字も重複してはいけない

の3つと、最初から数字が決まってるマスの情報。

あとはこれを yices へ渡してやると：

$ awk -f sudoku_solver.awk input_1.txt > to_yices.txt
$ yices to_yices.txt
sat
(= x56 3)
(= x59 1)
(= x61 7)
(= x18 1)
(= x33 8)
(= x98 7)
(= x71 9)
(= x86 9)
(= x62 1)
(= x35 4)
(= x48 2)
(= x65 2)
(= x52 2)
(= x74 5)
(= x25 9)
(= x82 8)
(= x11 5)
(= x44 7)
(= x39 7)
(= x49 3)
(= x54 8)
(= x77 2)
(= x91 3)
(= x79 4)
(= x94 2)
(= x83 7)
(= x38 6)
(= x95 8)
(= x87 6)
(= x28 4)
(= x53 6)
(= x21 6)
(= x81 2)
(= x45 6)
(= x46 1)
(= x64 9)
(= x58 9)
(= x43 9)
(= x42 5)
(= x31 1)
(= x73 1)
(= x24 1)
(= x36 2)
(= x72 6)
(= x16 8)
(= x97 1)
(= x99 9)
(= x69 6)
(= x17 9)
(= x89 5)
(= x26 5)
(= x92 4)
(= x93 5)
(= x85 1)
(= x37 5)
(= x68 5)
(= x23 2)
(= x96 6)
(= x32 9)
(= x41 8)
(= x51 4)
(= x88 3)
(= x75 3)
(= x13 4)
(= x27 3)
(= x67 8)
(= x34 3)
(= x76 7)
(= x63 3)
(= x84 4)
(= x15 7)
(= x55 5)
(= x66 4)
(= x29 8)
(= x47 4)
(= x57 7)
(= x14 6)
(= x78 8)
(= x12 3)
(= x19 2)
(= x22 7)

見難いので整形すると：

$ yices to_yices.txt > result.txt
$ sort result.txt  | awk '{ printf( "%d ", $3); if ( (NR % 9) == 0) printf( "\n" )
;}'
5 3 4 6 7 8 9 1 2
6 7 2 1 9 5 3 4 8
1 9 8 3 4 2 5 6 7
8 5 9 7 6 1 4 2 3
4 2 6 8 5 3 7 9 1
7 1 3 9 2 4 8 5 6
9 6 1 5 3 7 2 8 4
2 8 7 4 1 9 6 3 5
3 4 5 2 8 6 1 7 9
0

こんな感じ。
1秒かからずに解ける。

ちなみに yices はヤイクスと発音するらしい。色々応用出来そう。