ひとりにしてくれパズルをSugar制約ソルバーで解く

はじめに

Nikoliによる 「ひとりにしてくれ」(Hitori)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます．

例題

Nikoliによる ひとりにしてくれの例題 です．
例題
1862 6753
3111 8222
8324 7651
3758 3314
5446 7182
7143 2535
2283 4475
2231 4465

ひとりにしてくれのルール

Nikoliによる「ひとりにしてくれ」のルールは以下の通りです．
(Rule 1)
盤面に並んでいる数字のうち，余計なものを黒くぬって， タテ列，ヨコ列に同じ数字が重複しないようにします．
(Rule 2)
黒マスはタテヨコに連続しません． また，黒マスによって盤面が分断されることはありません．
「ひとりにしてくれ」を 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます．

なお，以下ではパズルの盤面の一番上の行を第0行， 一番左の列を第0列として数えます．

****************作成中****************

実行結果

すべての制約を記述したファイルを作成し， Sugarで実行すると以下のような結果が得られます． 
s SATISFIABLE
a x_0_0	1
a x_0_1	8
a x_0_2	0
a x_0_3	2
a x_0_4	6
a x_0_5	7
a x_0_6	5
a x_0_7	3
a x_1_0	3
a x_1_1	0
a x_1_2	1
a x_1_3	0
a x_1_4	8
a x_1_5	0
a x_1_6	2
a x_1_7	0
a x_2_0	8
a x_2_1	3
a x_2_2	2
a x_2_3	4
a x_2_4	7
a x_2_5	6
a x_2_6	0
a x_2_7	1
a x_3_0	0
a x_3_1	7
a x_3_2	5
a x_3_3	8
a x_3_4	3
a x_3_5	0
a x_3_6	1
a x_3_7	4
a x_4_0	5
a x_4_1	4
a x_4_2	0
a x_4_3	6
a x_4_4	0
a x_4_5	1
a x_4_6	8
a x_4_7	2
a x_5_0	7
a x_5_1	1
a x_5_2	4
a x_5_3	0
a x_5_4	2
a x_5_5	5
a x_5_6	3
a x_5_7	0
a x_6_0	2
a x_6_1	0
a x_6_2	8
a x_6_3	3
a x_6_4	4
a x_6_5	0
a x_6_6	7
a x_6_7	5
a x_7_0	0
a x_7_1	2
a x_7_2	3
a x_7_3	1
a x_7_4	0
a x_7_5	4
a x_7_6	6
a x_7_7	0
a z_0_0	59
a r_0_0	0
a z_0_1	58
a r_0_1	0
a z_0_2	0
a r_0_2	0
a z_0_3	58
a r_0_3	0
a z_0_4	59
a r_0_4	0
a z_0_5	58
a r_0_5	0
a z_0_6	57
a r_0_6	0
a z_0_7	56
a r_0_7	0
a z_1_0	60
a r_1_0	0
a z_1_1	0
a r_1_1	0
a z_1_2	62
a r_1_2	0
a z_1_3	0
a r_1_3	0
a z_1_4	60
a r_1_4	0
a z_1_5	0
a r_1_5	0
a z_1_6	56
a r_1_6	0
a z_1_7	0
a r_1_7	0
a z_2_0	61
a r_2_0	0
a z_2_1	62
a r_2_1	0
a z_2_2	63
a r_2_2	0
a z_2_3	60
a r_2_3	0
a z_2_4	61
a r_2_4	0
a z_2_5	60
a r_2_5	0
a z_2_6	0
a r_2_6	0
a z_2_7	50
a r_2_7	0
a z_3_0	0
a r_3_0	0
a z_3_1	63
a r_3_1	0
a z_3_2	64
a r_3_2	1
a z_3_3	63
a r_3_3	0
a z_3_4	62
a r_3_4	0
a z_3_5	0
a r_3_5	0
a z_3_6	50
a r_3_6	0
a z_3_7	51
a r_3_7	0
a z_4_0	61
a r_4_0	0
a z_4_1	62
a r_4_1	0
a z_4_2	0
a r_4_2	0
a z_4_3	62
a r_4_3	0
a z_4_4	0
a r_4_4	0
a z_4_5	54
a r_4_5	0
a z_4_6	53
a r_4_6	0
a z_4_7	52
a r_4_7	0
a z_5_0	60
a r_5_0	0
a z_5_1	61
a r_5_1	0
a z_5_2	60
a r_5_2	0
a z_5_3	0
a r_5_3	0
a z_5_4	56
a r_5_4	0
a z_5_5	55
a r_5_5	0
a z_5_6	52
a r_5_6	0
a z_5_7	0
a r_5_7	0
a z_6_0	59
a r_6_0	0
a z_6_1	0
a r_6_1	0
a z_6_2	59
a r_6_2	0
a z_6_3	58
a r_6_3	0
a z_6_4	57
a r_6_4	0
a z_6_5	0
a r_6_5	0
a z_6_6	51
a r_6_6	0
a z_6_7	50
a r_6_7	0
a z_7_0	0
a r_7_0	0
a z_7_1	55
a r_7_1	0
a z_7_2	56
a r_7_2	0
a z_7_3	57
a r_7_3	0
a z_7_4	0
a r_7_4	0
a z_7_5	49
a r_7_5	0
a z_7_6	50
a r_7_6	0
a z_7_7	0
a r_7_7	0
a
Sugarの次期リリースには， 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です． 以下は，その実行例です． 
$ ./hitori.pl data/hitori-0.txt >csp/hitori-0.csp

$ /usr/bin/time sugar csp/hitori-0.csp >log/hitori-0.log
2.74user 0.12system 0:01.84elapsed 155%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+928outputs (2major+14551minor)pagefaults 0swaps

$ ./hitori.pl -s log/hitori-0.log data/hitori-0.txt
; Hitori Puzzle
; # http://www.nikoli.co.jp/en/puzzles/hitori/
; size 8 8
; 1 8 6 2 6 7 5 3
; 3 1 1 1 8 2 2 2
; 8 3 2 4 7 6 5 1
; 3 7 5 8 3 3 1 4
; 5 4 4 6 7 1 8 2
; 7 1 4 3 2 5 3 5
; 2 2 8 3 4 4 7 5
; 2 2 3 1 4 4 6 5

 1  8 ### 2  6  7  5  3 
 3 ### 1 ### 8 ### 2 ###
 8  3  2  4  7  6 ### 1 
### 7  5  8  3 ### 1  4 
 5  4 ### 6 ### 1  8  2 
 7  1  4 ### 2  5  3 ###
 2 ### 8  3  4 ### 7  5 
### 2  3  1 ### 4  6 ###

; END
以下は， Nikoli: ひとりにしてくれのおためし問題中の おためし問題10 (17x17)をLet's Note CF-W5で解いた結果です(MiniSat2を使用)． 15秒程度で解けています(CPU時間は約20秒)． 
$ ./hitori.pl data/hitori-10.txt >csp/hitori-10.csp

$ /usr/bin/time sugar csp/hitori-10.csp >log/hitori-10.log
18.80user 0.42system 0:14.08elapsed 136%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+19088outputs (2major+43212minor)pagefaults 0swaps

$ ./hitori.pl -s log/hitori-10.log data/hitori-10.txt
; Hitori Puzzle
; # http://www.nikoli.co.jp/en/puzzles/hitori/
; size 17 17
;  1  6  6  3  2  4  7  8 16 11  9 10 16 12  5 13  5
;  2  3  4  9  1 17  6 10 16 10  5  7 11 17  8 14 12
;  8  2  5  4  8  1 17  7 16  3  6  9 10 11  5 12  5
;  3  9  8  5  4  9 17 10  1  7 11  7  6 13  2 14 15
;  8  4 13  6  5  2 17  1  8 12 13 11  8 14  7  9 13
;  4  1  3  9  6  9  8  2  5  2 10  7 12 15 11 15 14
;  8  5  7 11 15 12  1  4  2 13  6 14 16  9  3 10 17
;  5  7  2 12  9 13  3 15 10  2  1  2 14 16  4  2  6
; 17 16 10 14  5  6 13 13 13  4  3 12  7 16  7 11  9
; 17 16  9  8  7 13  2 15  3  8 12  8  5 16  6  8  4
;  6  8 17 13 15  5 15 11  7 14  2  4 16 10  7  3  9
;  7  1 17  1 11  3  9  3 12  1  8  1 15  3 13 14 10
;  9 10 17  7  5  8  5 12  6 15  2 16  1  1  1  4  3
; 12 12 11 10 10 10 14 15 17  9  7  3 13  3 16  2  2
; 11 11 12 15 13  7  5 14  6  9  6 17  2  2 10  1  1
; 10 13  1  2  3 11 12  5 14  9 15  7  4  6 17 16  8
; 12 14  1  2  3 15  4  6  4  5  4 13 16  7 17 16 11

 1 ### 6  3  2  4  7  8 ###11  9 10 ###12  5 13 ###
 2  3  4 ### 1 ### 6 ###16 10  5 ###11 17  8 ###12 
### 2 ### 4  8  1 ### 7 ### 3 ### 9 10 11 ###12  5 
 3 ### 8  5  4  9 17 10  1  7 11 ### 6 13  2 ###15 
 8  4 ### 6 ### 2 ### 1 ###12 ###11 ###14 ### 9 13 
 4  1  3  9  6 ### 8 ### 5  2 10  7 12 15 11 ###14 
### 5  7 11 ###12  1  4  2 13 ###14 ### 9  3 10 17 
 5  7 ###12  9 ### 3 ###10 ### 1  2 14 ### 4 ### 6 
17 ###10 14 ### 6 ###13 ### 4  3 12  7 16 ###11  9 
###16  9 ### 7 13  2 15  3  8 12 ### 5 ### 6 ### 4 
 6  8 ###13 15  5 ###11 ###14 ### 4 16 10  7  3 ###
 7 ###17  1 11 ### 9  3 12 ### 8 ###15 ###13 14 10 
 9 10 ### 7  5  8 ###12  6 15  2 16 ### 1 ### 4  3 
12 ###11 ###10 ###14 ###17 ### 7 ###13  3 16 ### 2 
###11 12 15 13  7  5 14 ### 9  6 17  2 ###10  1 ###
10 13 ### 2 ###11 12  5 14 ###15 ### 4  6 ###16  8 
###14  1 ### 3 15 ### 6 ### 5  4 13 ### 7 17 ###11 

; END

「パズルをSugar制約ソルバーで解く」に戻る

Naoyuki Tamura