フィルオミノ・パズルをSugar制約ソルバーで解く


はじめに

Nikoliによる フィルオミノ(Fillomino)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます.

例題

Nikoliによる フィルオミノの例題 です.
例題
 2  4 2  
1 2  6  6
3   3   3
    5    
3   2   3
3 2  4  2
 3  3 1  

フィルオミノのルール

Nikoliによるフィルオミノのルールは以下の通りです.
(Rule 1)
すべてのマスに数字を1つずつ入れます.
(Rule 2)
タテヨコにつながった同じ数字が入るマスを1つのブロックとし,全体をいくつかに分割します.
(Rule 3)
1つのブロックのマスの数は,そのブロックに入っている数字と同じでなければいけません.
(Rule 4)
同じ数字のブロックは辺を共有してはいけません.
フィルオミノを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

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

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

実行結果

すべての制約を記述したファイルを作成し, Sugarで実行すると以下のような結果が得られます.
s SATISFIABLE
a x_0_0	2
a x_0_1	2
a x_0_2	4
a x_0_3	4
a x_0_4	4
a x_0_5	2
a x_0_6	2
a x_1_0	1
a x_1_1	3
a x_1_2	2
a x_1_3	4
a x_1_4	6
a x_1_5	6
a x_1_6	6
a x_2_0	3
a x_2_1	3
a x_2_2	2
a x_2_3	3
a x_2_4	3
a x_2_5	6
a x_2_6	3
a x_3_0	5
a x_3_1	5
a x_3_2	5
a x_3_3	5
a x_3_4	3
a x_3_5	6
a x_3_6	3
a x_4_0	3
a x_4_1	3
a x_4_2	5
a x_4_3	2
a x_4_4	2
a x_4_5	6
a x_4_6	3
a x_5_0	3
a x_5_1	2
a x_5_2	2
a x_5_3	4
a x_5_4	4
a x_5_5	4
a x_5_6	2
a x_6_0	1
a x_6_1	3
a x_6_2	3
a x_6_3	3
a x_6_4	4
a x_6_5	1
a x_6_6	2
a v_0_0	0
a h_0_0	1
a r_0_0	0
a q_0_0	2
a c_0_0	1
a v_0_1	0
a h_0_1	0
a r_0_1	1
a q_0_1	2
a c_0_1	2
a v_0_2	0
a h_0_2	1
a r_0_2	0
a q_0_2	11
a c_0_2	1
a v_0_3	1
a h_0_3	-1
a r_0_3	0
a q_0_3	11
a c_0_3	3
a v_0_4	0
a h_0_4	0
a r_0_4	0
a q_0_4	11
a c_0_4	1
a v_0_5	0
a h_0_5	1
a r_0_5	0
a q_0_5	7
a c_0_5	1
a v_0_6	0
a r_0_6	1
a q_0_6	7
a c_0_6	2
a v_1_0	0
a h_1_0	0
a r_1_0	1
a q_1_0	8
a c_1_0	1
a v_1_1	-1
a h_1_1	0
a r_1_1	1
a q_1_1	9
a c_1_1	3
a v_1_2	1
a h_1_2	0
a r_1_2	0
a q_1_2	17
a c_1_2	1
a v_1_3	0
a h_1_3	0
a r_1_3	1
a q_1_3	11
a c_1_3	4
a v_1_4	0
a h_1_4	1
a r_1_4	0
a q_1_4	34
a c_1_4	1
a v_1_5	1
a h_1_5	-1
a r_1_5	0
a q_1_5	34
a c_1_5	3
a v_1_6	0
a r_1_6	0
a q_1_6	34
a c_1_6	1
a v_2_0	0
a h_2_0	1
a r_2_0	0
a q_2_0	9
a c_2_0	1
a v_2_1	0
a h_2_1	0
a r_2_1	0
a q_2_1	9
a c_2_1	2
a v_2_2	0
a h_2_2	0
a r_2_2	1
a q_2_2	17
a c_2_2	2
a v_2_3	0
a h_2_3	1
a r_2_3	0
a q_2_3	26
a c_2_3	1
a v_2_4	1
a h_2_4	0
a r_2_4	0
a q_2_4	26
a c_2_4	2
a v_2_5	1
a h_2_5	0
a r_2_5	0
a q_2_5	34
a c_2_5	4
a v_2_6	1
a r_2_6	0
a q_2_6	35
a c_2_6	1
a v_3_0	0
a h_3_0	1
a r_3_0	0
a q_3_0	25
a c_3_0	1
a v_3_1	0
a h_3_1	1
a r_3_1	0
a q_3_1	25
a c_3_1	2
a v_3_2	-1
a h_3_2	1
a r_3_2	0
a q_3_2	25
a c_3_2	4
a v_3_3	0
a h_3_3	0
a r_3_3	1
a q_3_3	25
a c_3_3	5
a v_3_4	0
a h_3_4	0
a r_3_4	1
a q_3_4	26
a c_3_4	3
a v_3_5	1
a h_3_5	0
a r_3_5	0
a q_3_5	34
a c_3_5	5
a v_3_6	1
a r_3_6	0
a q_3_6	35
a c_3_6	2
a v_4_0	-1
a h_4_0	1
a r_4_0	0
a q_4_0	30
a c_4_0	2
a v_4_1	0
a h_4_1	0
a r_4_1	1
a q_4_1	30
a c_4_1	3
a v_4_2	0
a h_4_2	0
a r_4_2	0
a q_4_2	25
a c_4_2	1
a v_4_3	0
a h_4_3	1
a r_4_3	0
a q_4_3	33
a c_4_3	1
a v_4_4	0
a h_4_4	0
a r_4_4	1
a q_4_4	33
a c_4_4	2
a v_4_5	0
a h_4_5	0
a r_4_5	1
a q_4_5	34
a c_4_5	6
a v_4_6	0
a r_4_6	1
a q_4_6	35
a c_4_6	3
a v_5_0	0
a h_5_0	0
a r_5_0	0
a q_5_0	30
a c_5_0	1
a v_5_1	0
a h_5_1	1
a r_5_1	0
a q_5_1	38
a c_5_1	1
a v_5_2	0
a h_5_2	0
a r_5_2	1
a q_5_2	38
a c_5_2	2
a v_5_3	0
a h_5_3	1
a r_5_3	0
a q_5_3	47
a c_5_3	1
a v_5_4	1
a h_5_4	-1
a r_5_4	0
a q_5_4	47
a c_5_4	3
a v_5_5	0
a h_5_5	0
a r_5_5	0
a q_5_5	47
a c_5_5	1
a v_5_6	1
a r_5_6	0
a q_5_6	49
a c_5_6	1
a h_6_0	0
a r_6_0	1
a q_6_0	43
a c_6_0	1
a h_6_1	1
a r_6_1	0
a q_6_1	46
a c_6_1	1
a h_6_2	1
a r_6_2	0
a q_6_2	46
a c_6_2	2
a h_6_3	0
a r_6_3	1
a q_6_3	46
a c_6_3	3
a h_6_4	0
a r_6_4	1
a q_6_4	47
a c_6_4	4
a h_6_5	0
a r_6_5	1
a q_6_5	48
a c_6_5	1
a r_6_6	1
a q_6_6	49
a c_6_6	2
a
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です. 以下は,その実行例です.
$ ./fillomino.pl data/fillomino-0.txt >csp/fillomino-0.csp

$ /usr/bin/time sugar csp/fillomino-0.csp >log/fillomino-0.log
6.24user 0.17system 0:03.65elapsed 175%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+1800outputs (2major+24178minor)pagefaults 0swaps

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

 2  2  4  4  4  2  2 
 1  3  2  4  6  6  6 
 3  3  2  3  3  6  3 
 5  5  5  5  3  6  3 
 3  3  5  2  2  6  3 
 3  2  2  4  4  4  2 
 1  3  3  3  4  1  2 

; END

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


Naoyuki Tamura