美術館パズルを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に従い,次のようにします. 変数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

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


Naoyuki Tamura
( Last modified: Sun Jun 8 14:47:03 2008 JST ,   ?????  Since June 4, 2008 )