美術館パズルをSugar制約ソルバーで解く

はじめに

Nikoliによる美術館(Akari, Light Up)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます．

例題

Nikoliによる美術館の例題です．例題

		1
3
			0

	4			0
2
		1

美術館のルール

Nikoliによる美術館のルールは以下の通りです．

(Rule 1): 以下のルールに従って盤面の白マスに○(照明)を配置します．
(Rule 2): 数字は，タテヨコ両隣の最大4つの白マスに入る○の数を表します．
(Rule 3): 照明は，そのマスから上下左右に，黒マスか外枠にぶつかるまでの範囲を照らします．ナナメには照らせません．
(Rule 4): どの照明にも照らされてない白マスがあってはいけません．また，照明のあるマスは，他の照明で照らされてはいけません．

美術館を制約充足問題(CSP, Constraint Satisfaction Problem)として表すための方法について考えていきます．

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

Rule 1

(Rule 1): 以下のルールに従って盤面の白マスに○(照明)を配置します．

Ruleに従い，次のようにします．

各白マスに0か1の値を取る変数を割り当てて， 1の場合に照明を配置することを表すようにします．
i 行目，j 列目の白マスに変数x_i_jを割り当てます．すなわち，一番左上のマスがx_0_0，その右のマスがx_0_1，一番右下のマスがx_7_7となります．
白でないマスには変数を割り当てません．たとえば，x_1_1は用いません．

変数x_0_0は，0か1の値のいずれかを取るので，以下のように宣言します．

    (int x_0_0 0 1)  ; 0行目0列目は0か1のいずれかの値が入る

他の変数も同様に宣言します．

Rule 2

(Rule 2): 数字は，タテヨコ両隣の最大4つの白マスに入る○の数を表します．

たとえば，0行目5列目には1の数字が入っています．タテヨコ両隣の白マスに対応する変数は， x_0_4, x_0_6, x_1_5の3つです．したがって，それらの変数の和が1に等しいという以下の制約条件を追加します．

    (= (+ x_0_4 x_0_6 x_1_5) 1)

他の数字のマスについても同様にします．

Rule 3とRule 4

(Rule 3): 照明は，そのマスから上下左右に，黒マスか外枠にぶつかるまでの範囲を照らします．ナナメには照らせません．
(Rule 4): どの照明にも照らされてない白マスがあってはいけません．また，照明のあるマスは，他の照明で照らされてはいけません．

まず，最後の「照明のあるマスは，他の照明で照らされてはいけません」という Ruleについて考えます．このRuleは，上下あるいは左右に連続している白マス中には， 2つ以上の照明があってはならないことを表します．たとえば，0行目0列目から2行目0列目まで連続している白マス中に入る照明の個数は， 1つ以下となります．また，0行目0列目から0行目4列目まで連続している白マス中に入る照明の個数も， 1つ以下となります．これらは，次のような制約条件で表されます．

  (<= (+ x_0_0 x_1_0 x_2_0) 1)
  (<= (+ x_0_0 x_0_1 x_0_2 x_0_3 x_0_4) 1)

他の連続する白マスについても同様にします．

次に，「どの照明にも照らされてない白マスがあってはいけません」という Ruleについて考えます．たとえば，2行目3列目の白マスを見てみます．この白マスが照らされるためには，以下で黄色で示されるマス中に照明がなければいけません (照明が2つあっても良いことに注意)．

		1
3
			0

	4			0
2
		1

すなわち，これらの白マス中にある照明の個数が1以上であれば良いわけです．これは，次のような制約条件で表されます．

    (>= (+ x_2_3 x_1_3 x_0_3 x_2_2 x_2_1 x_2_0 x_2_4 x_2_5 x_3_3) 1)

他の白マスについても同様にします．

実行結果

すべての制約を記述したファイルを作成し， Sugarで実行すると以下のような結果が得られます．

s SATISFIABLE
a x_0_0	0
a x_0_1	1
a x_0_2	0
a x_0_3	0
a x_0_4	0
a x_0_6	1
a x_0_7	0
a x_1_0	1
a x_1_3	0
a x_1_4	0
a x_1_5	0
a x_1_6	0
a x_1_7	1
a x_2_0	0
a x_2_1	1
a x_2_2	0
a x_2_3	0
a x_2_4	0
a x_2_5	0
a x_2_7	0
a x_3_1	0
a x_3_2	0
a x_3_3	1
a x_3_5	1
a x_3_6	0
a x_3_7	0
a x_4_0	0
a x_4_1	0
a x_4_2	1
a x_4_4	1
a x_4_5	0
a x_4_6	0
a x_5_0	1
a x_5_2	0
a x_5_3	1
a x_5_4	0
a x_5_5	0
a x_5_6	0
a x_5_7	0
a x_6_0	0
a x_6_1	1
a x_6_2	0
a x_6_3	0
a x_6_4	0
a x_7_0	0
a x_7_1	0
a x_7_3	0
a x_7_4	0
a x_7_5	1
a x_7_6	0
a x_7_7	0
a

Sugarの次期リリースには，問題ファイルを読み込んで制約条件を記述したCSPファイルを作成するツールを含める予定です．以下は，その実行例です．

$ ./akari.pl data/akari-0.txt >csp/akari-0.csp

$ /usr/bin/time sugar csp/akari-0.csp >log/akari-0.log
0.72user 0.07system 0:00.73elapsed 108%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+152outputs (2major+9112minor)pagefaults 0swaps

$ ./akari.pl -s log/akari-0.log data/akari-0.txt
; Akari (Light Up) Puzzle
; # http://www.nikoli.co.jp/en/puzzles/akari/
; size 8 8
; - - - - - 1 - -
; - 3 X - - - - -
; - - - - - - 0 -
; X - - - X - - -
; - - - 4 - - - 0
; - 2 - - - - - -
; - - - - - 1 X 0
; - - X - - - - -

 -  @  -  -  -  1  @  -
 @  3  X  -  -  -  -  @
 -  @  -  -  -  -  0  -
 X  -  -  @  X  @  -  -
 -  -  @  4  @  -  -  0
 @  2  -  @  -  -  -  -
 -  @  -  -  -  1  X  0
 -  -  X  -  -  @  -  -

; END

以下は， Nikoli: 美術館のおためし問題中のおためし問題10 (36x20)をLet's Note CF-W5で解いた結果です(MiniSat2を使用)． 5秒以内で解けています(CPU時間は約9秒)．

$ ./akari.pl data/akari-10.txt >csp/akari-10.csp

$ /usr/bin/time sugar csp/akari-10.csp >log/akari-10.log
8.78user 0.21system 0:04.84elapsed 185%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+760outputs (2major+29538minor)pagefaults 0swaps

$ ./akari.pl -s log/akari-10.log data/akari-10.txt
; Akari (Light Up) Puzzle
; # http://www.nikoli.co.jp/en/puzzles/akari/
; size 36 20
; - - 2 - - - - - - - - - - - X - - - - - - - - - - - 1 - - - - - - - - -
; - - - 2 - - - - - 3 - - - - - X - - - - - 3 - - - - - X - - - - - 1 - -
; X - - - 2 - - - 3 - - - X - - - X - - - 1 - - - 2 - - - 2 - - - 1 - - -
; - - - - - - 1 1 - - X - - - - - - - 1 1 - - 1 - - - - - - - 1 1 - - 1 -
; - X - - 2 1 - - - - - - - X - - 2 1 - - - - - - - 1 - - 1 1 - - - - - -
; - - - 2 - - - X - - - 0 - - - 2 - - - X - - - X - - - 1 - - - 1 - - - X
; - - 1 - - - - - 0 - - - - - 3 - - - - - 2 - - - - - 1 - - - - - 1 - - -
; - 2 - - - - - - - X - - - 3 - - - - - - - X - - - 1 - - - - - - - 1 - -
; 2 - - - - - 1 - - - X - 2 - - - - - 0 - - - 3 - 1 - - - - - 1 - - - 2 -
; 1 - - - 1 - - - - - - - 1 - - - X - - - - - - - 1 - - - 1 - - - - - - -
; - - - - - - - 1 - - - 1 - - - - - - - 1 - - - 1 - - - - - - - 1 - - - 1
; - X - - - X - - - - - 1 - X - - - X - - - - - 1 - 3 - - - 1 - - - - - 1
; - - 1 - - - - - - - 3 - - - X - - - - - - - 1 - - - 3 - - - - - - - 1 -
; - - - X - - - - - 2 - - - - - 1 - - - - - 1 - - - - - 1 - - - - - 1 - -
; 1 - - - 2 - - - 1 - - - 2 - - - 0 - - - 1 - - - 2 - - - X - - - 3 - - -
; - - - - - - 2 1 - - X - - - - - - - 1 1 - - X - - - - - - - 1 2 - - X -
; - 1 - - 2 1 - - - - - - - 2 - - 1 1 - - - - - - - 0 - - 2 1 - - - - - -
; - - - 1 - - - X - - - X - - - 1 - - - 1 - - - X - - - 2 - - - X - - - X
; - - 2 - - - - - 1 - - - - - 1 - - - - - X - - - - - 0 - - - - - 1 - - -
; - - - - - - - - - 1 - - - - - - - - - - - 1 - - - - - - - - - - - 2 - -

 @  -  2  @  -  -  -  -  -  -  -  -  -  -  X  -  -  -  -  -  -  @  -  -  -  -  1  @  -  -  -  -  -  -  -  - 
 -  -  @  2  -  -  -  -  @  3  @  -  -  -  -  X  -  -  -  -  @  3  @  -  -  -  -  X  @  -  -  -  -  1  @  - 
 X  @  -  -  2  @  -  -  3  @  -  -  X  @  -  -  X  -  @  -  1  -  -  @  2  -  -  @  2  -  -  @  1  -  -  @ 
 -  -  -  -  @  -  1  1  @  -  X  -  -  -  -  -  @  -  1  1  -  @  1  -  @  -  -  -  -  -  1  1  -  @  1  - 
 -  X  -  @  2  1  @  -  -  -  -  -  -  X  -  @  2  1  -  @  -  -  -  -  -  1  @  -  1  1  @  -  -  -  -  - 
 -  @  -  2  -  -  -  X  -  -  -  0  -  -  @  2  -  @  -  X  @  -  -  X  -  -  -  1  @  -  -  1  @  -  -  X 
 -  -  1  @  -  -  -  -  0  -  -  -  -  @  3  -  -  -  -  @  2  -  -  -  -  @  1  -  -  -  -  -  1  -  @  - 
 @  2  -  -  @  -  -  -  -  X  @  -  -  3  @  -  -  -  -  -  -  X  @  -  -  1  -  -  -  -  -  -  -  1  -  - 
 2  @  -  -  -  -  1  @  -  -  X  @  2  @  -  -  -  -  0  -  -  @  3  @  1  -  -  -  -  @  1  -  -  @  2  @ 
 1  -  -  -  1  @  -  -  -  -  -  -  1  -  -  -  X  -  -  -  @  -  -  -  1  @  -  -  1  -  -  @  -  -  -  - 
 @  -  -  -  -  -  -  1  @  -  -  1  @  -  -  -  -  -  -  1  -  -  @  1  -  -  -  -  @  -  -  1  -  -  @  1 
 -  X  @  -  -  X  -  -  -  -  @  1  -  X  -  -  @  X  -  @  -  -  -  1  @  3  @  -  -  1  @  -  -  -  -  1 
 -  -  1  -  -  -  -  -  -  @  3  -  -  -  X  @  -  -  -  -  -  -  1  -  -  @  3  @  -  -  -  -  -  -  1  @ 
 -  -  -  X  @  -  -  -  -  2  @  -  -  -  -  1  -  -  @  -  -  1  @  -  -  -  -  1  -  -  -  -  @  1  -  - 
 1  @  -  -  2  -  @  -  1  -  -  @  2  @  -  -  0  -  -  -  1  -  -  @  2  -  @  -  X  -  -  @  3  -  @  - 
 -  -  -  -  @  -  2  1  @  -  X  -  -  -  -  -  -  @  1  1  @  -  X  -  @  -  -  -  -  -  1  2  @  -  X  - 
 -  1  @  -  2  1  @  -  -  -  -  -  -  2  @  -  1  1  -  -  -  -  @  -  -  0  -  @  2  1  @  -  -  -  -  - 
 @  -  -  1  @  -  -  X  -  -  @  X  -  @  -  1  @  -  -  1  -  -  -  X  -  -  -  2  @  -  -  X  -  -  -  X 
 -  @  2  -  -  @  -  -  1  @  -  -  -  -  1  -  -  -  -  @  X  @  -  -  -  -  0  -  -  @  -  -  1  @  -  - 
 -  -  @  -  -  -  -  -  -  1  -  -  -  -  @  -  -  -  -  -  -  1  -  -  -  @  -  -  -  -  -  -  -  2  @  - 

; END

Akari Solver in Copris も参照してください．

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

Naoyuki Tamura