橋をかけろパズルをSugar制約ソルバーで解く


はじめに

Nikoliによる 橋をかけろ(Hashiwokakero, Bridges)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます.

例題

Nikoliによる 橋をかけろの例題 です.
例題
4 3  3  3
 2    4  
3   3   3
         
2   8 4  
     1  3
 1  4 1  

橋をかけろのルール

Nikoliによる橋をかけろのルールは以下の通りです.
(Rule 1)
数字から数字に橋をかけて,全体をつなげます.
(Rule 2)
数字は,その数字につながる橋の数です.
(Rule 3)
橋はタテヨコにかけます.ナナメや,数字をとびこえてはかけられません.
(Rule 4)
橋は1カ所に2本までかけられます.
(Rule 5)
橋どうしが交差してはいけません.
橋をかけろを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

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

Rule 1とRule 3とRule 4

(Rule 1)
数字から数字に橋をかけて,全体をつなげます.
(Rule 3)
橋はタテヨコにかけます.ナナメや,数字をとびこえてはかけられません.
(Rule 4)
橋は1カ所に2本までかけられます.
ましゅパズルをSugar制約ソルバーで解く」や 「スリザーリンク・パズルをSugar制約ソルバーで解く」の 時と同様に,このRule中の「全体をつなげます」という条件が一番面倒ですので, この部分は後回し,全体がつながっていなくても良いことにして話を進めます. 次に数字(節点)とその上下左右にある数字(節点)を結ぶ辺(edge)に変数を割り当てます. 上下左右に数字がない場合は,辺の変数は割り当てません. これらの辺を表す変数は,橋の本数を表すのであれば, 0から2の値を取れば良いのですが,後述の処理のため, 橋の向きを含めて表現できるようにし,-2から2の値を取ることにします.

たとえば,節点n_0_0から下への辺v_0_0および 右への辺h_0_0の宣言は以下のようになります.

    (int v_0_0 -2 2)  ; n_0_0からn_2_0への辺
    (int h_0_0 -2 2)  ; n_0_0からn_0_2への辺
他の辺を表す変数についても同様に宣言します.

Rule 2

(Rule 2)
数字は,その数字につながる橋の数です.

たとえば,数字8の書いてあるn_4_3の節点について考えます. この節点につながる辺は, v_4_3 (下への辺), h_4_3 (右への辺), v_2_3 (上への辺), h_4_0 (左への辺)の4つです. それぞれの橋の本数は,絶対値関数absで求めることができますから, 以下のような制約条件となります.

    (= (+ (abs v_4_3) (abs h_4_3) (abs v_2_3) (abs h_4_0)) 8)
他の数字についても同様に制約条件を記述します.

Rule 2

(Rule 5)
橋どうしが交差してはいけません.

たとえば, v_1_1 (数字2のn_1_1の節点から下への辺)と h_2_0 (数字3のn_2_0の節点から右への辺)とは 交差してはいけません.すなわち,少なくともどちらかの値が0となります. これを制約条件として書くと以下のようになります.

    (or (= v_1_1 0) (= h_2_0 0))
他の交差する可能性のある辺の組み合わせについても同様に記述します.

Rule 1 再び

(Rule 1)
数字から数字に橋をかけて,全体をつなげます.
最後に再びRule 1の「全体をつなげます」という条件を考えます.

ましゅパズルをSugar制約ソルバーで解く」や 「スリザーリンク・パズルをSugar制約ソルバーで解く」の 時は, つながっている部分(グラフ理論では,連結成分といいます)のそれぞれについて, 節点に番号を付けることによって始節点を決めることができました.

「橋をかけろ」の場合も同様に考えることができます.

まず,各連結成分は,辺の向きをうまく選べば, Rooted DAG (Rooted Directed Acyclic Graph)にできます. Rooted DAGとは....,ちゃんとした説明は面倒ですね...

では,こうしましょう.各橋が伸縮自在なゴムでできていると想像してください. また,どれかの数字をつまんで,紙から持ち上げることができると考えてください. 持ち上げた数字につながって,橋や他の数字も持ち上がります.

その時,持ち上げた全体がRooted DAGになっています! つまんでいる数字が根(root)の節点で, 各辺は上の数字から下の数字に向いているとすれば, 向きに沿って辺をたどっていってもループが存在しないのでacyclicですね.

各連結成分をRooted DAGにできれば, 「根の節点がちょうど1つ」という条件により,連結成分を一つにできます.

そこで,まず以下の変数を用意します.

たとえば,節点n_0_0について,以下の宣言を加えます.
    (int z_0_0 1 17)
    (int r_0_0 0 1)
さらに, z_0_0が1に等しい時だけr_0_0が1に等しくなるという条件を 加えます.
    (iff (= z_0_0 1) (= r_0_0 1))
他の節点についても同様にします.

次に,すべてのr_i_jの和が1に等しいという条件を加え, 「根の節点がちょうど1つ」すなわち「全体がつながっている」という条件を表します.

    (= (+ r_0_0 r_0_2 ... r_6_5) 1)
****************作成中****************
    (=> (> v_4_3 0) (< z_4_3 z_6_3))
    (=> (> h_4_3 0) (< z_4_3 z_4_5))
    (=> (< v_2_3 0) (< z_4_3 z_2_3))
    (=> (< h_4_0 0) (< z_4_3 z_4_0))
    (=> (= r_4_3 0) (or (< v_4_3 0) (< h_4_3 0) (> v_2_3 0) (> h_4_0 0)))

実行結果

すべての制約を記述したファイルを作成し, Sugarで実行すると以下のような結果が得られます.
s SATISFIABLE
a v_0_0	2
a h_0_0	2
a h_0_2	1
a v_0_4	0
a h_0_4	2
a v_0_6	1
a v_1_1	0
a h_1_1	-2
a v_1_5	-2
a v_2_0	0
a h_2_0	1
a v_2_3	2
a h_2_3	0
a v_2_6	2
a h_4_0	-2
a v_4_3	2
a h_4_3	2
a v_4_5	0
a h_5_4	-1
a h_6_1	-1
a h_6_3	1
a z_0_0	1
a r_0_0	1
a z_0_2	12
a r_0_2	0
a z_0_4	13
a r_0_4	0
a z_0_6	14
a r_0_6	0
a z_1_1	17
a r_1_1	0
a z_1_5	16
a r_1_5	0
a z_2_0	12
a r_2_0	0
a z_2_3	13
a r_2_3	0
a z_2_6	15
a r_2_6	0
a z_4_0	17
a r_4_0	0
a z_4_3	14
a r_4_3	0
a z_4_5	15
a r_4_5	0
a z_5_4	17
a r_5_4	0
a z_5_6	16
a r_5_6	0
a z_6_1	17
a r_6_1	0
a z_6_3	16
a r_6_3	0
a z_6_5	17
a r_6_5	0
a
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です. 以下は,その実行例です.
$ ./hashiwokakero.pl data/hashiwokakero-0.txt >csp/hashiwokakero-0.csp

$ /usr/bin/time sugar csp/hashiwokakero-0.csp >log/hashiwokakero-0.log
0.98user 0.11system 0:00.91elapsed 119%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+176outputs (2major+9809minor)pagefaults 0swaps

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

 4 === 3 --- 3 === 3  
 #  2 ========= 4  |  
 3 ------ 3     #  3  
          #     #  #  
 2 ====== 8 === 4  #  
          #  1 --- 3  
    1 --- 4 --- 1     

; END
以下は, Nikoli: 橋をかけろのおためし問題中の おためし問題10 (32x18)をLet's Note CF-W5で解いた結果です(MiniSat2を使用). 10秒程度で解けています.
$ ./hashiwokakero.pl data/hashiwokakero-10.txt >csp/hashiwokakero-10.csp

$ /usr/bin/time sugar csp/hashiwokakero-10.csp >log/hashiwokakero-10.log
9.38user 0.31system 0:06.98elapsed 138%CPU (0avgtext+0avgdata 0maxresident)k
21120inputs+8272outputs (103major+30910minor)pagefaults 0swaps

$ ./hashiwokakero.pl -s log/hashiwokakero-10.log data/hashiwokakero-10.txt
; Hashiwokakero Puzzle
; # http://www.nikoli.co.jp/en/puzzles/hashiwokakero/
; size 32 18
;  3 - 3 - 4 - 3 - - - 4 - 3 - - 3 - 4 - - 3 - 4 - - 1 - 3 - 3 - 2
;  - 2 - 3 - 5 - - 3 - - 2 - 4 - - 1 - 2 - - 3 - 2 - - 3 - 3 - 2 -
;  2 - - - 1 - - - - - 3 - 1 - 2 - - 5 - 1 - - 1 - 1 - - 1 - - - -
;  - 3 - 1 - - 2 - 3 - - 2 - 3 - - 1 - - - - 4 - 3 - 1 - - - 2 - 4
;  - - - - - 2 - 3 - - 4 - - - - - - 2 - 1 - - - - - - 3 - 5 - 1 -
;  1 - 3 - 4 - 4 - - 4 - 1 - - 3 - 5 - 2 - - 5 - - 3 - - - - 1 - 4
;  - 1 - - - - - - - - 2 - - 3 - - - 2 - - 1 - - 2 - 4 - - 6 - 3 -
;  4 - 5 - - 1 - 2 - 6 - - 1 - 1 - - - - 3 - 3 - - 1 - 1 - - - - 3
;  - 2 - - 3 - 4 - 1 - - 3 - 4 - - 5 - - - 2 - - 5 - - - 1 - - 2 -
;  2 - 2 - - 3 - 2 - - - - 3 - - 1 - 4 - 6 - - 2 - 3 - 2 - 3 - - 4
;  - 3 - - 3 - 2 - - 4 - 3 - - - - - - 1 - 1 - - - - 2 - 4 - - 2 -
;  - - - 1 - 3 - - 5 - - - 5 - 3 - 4 - - 2 - - - 2 - - 3 - - 2 - 3
;  3 - 2 - - - - 2 - - 3 - - 2 - - - 1 - - - - 4 - 3 - - - - - - -
;  - - - - 3 - 2 - 2 - - 3 - - 3 - 4 - 5 - 3 - - 1 - - 4 - 3 - 4 -
;  3 - - 5 - 4 - 5 - - 4 - - - - - - - - 1 - - 4 - - 2 - 3 - 1 - 3
;  - - - - - - - - 1 - - 3 - 2 - - 2 - 4 - - 4 - - 4 - 3 - - - 1 -
;  3 - 2 - - 1 - 1 - - - - - - 3 - - 3 - 1 - - - - - 1 - 4 - 2 - 2
;  - 2 - 3 - - 2 - 4 - 5 - - 4 - 1 - - 2 - - 3 - - 3 - 3 - 3 - 2 -

 3 --- 3 === 4 === 3 --------- 4 === 3 ------ 3 === 4 ------ 3 === 4 ------ 1     3 === 3 --- 2  
 #  2 --- 3 === 5 ====== 3     |  2 === 4 ------ 1  |  2 ====== 3  |  2 ------ 3  |  3 === 2  |  
 2  |        1  |        |     3 --- 1  |  2 ====== 5 --- 1     |  1  |  1     #  1  |        |  
    3 --- 1  |  |  2 === 3     |  2 --- 3        1  |           4 === 3  |  1  #     |  2 === 4  
    |        |  2 --- 3 ====== 4  |     |        |  2 --- 1     |        |  |  3 --- 5 --- 1  |  
 1  |  3 === 4 --- 4 ====== 4  |  1     |  3 === 5 --- 2 ------ 5 ====== 3  |        #  1 --- 4  
 |  1  |           |        #  2 ------ 3  |     |  2 ------ 1  |     2 --- 4 ====== 6 --- 3  #  
 4 --- 5 ------ 1  |  2 === 6 ------ 1  |  1     |  |     3 === 3     |  1     1     |     #  3  
 #  2  #     3 === 4 --- 1  |     3 --- 4 ====== 5  |     |  2 ====== 5  |     |  1  |     2  |  
 2  #  2     |  3 === 2     |     #  3 ------ 1  #  4 === 6 ------ 2  #  3 --- 2  |  3 ====== 4  
    3 ------ 3  |  2 ====== 4 --- 3  #           #  |  1  #  1     |  #  |  2 === 4 ------ 2  |  
          1  |  3 ====== 5 --------- 5 === 3 --- 4  |  |  2  |     |  2  |     3 ====== 2  |  3  
 3 === 2  |  |        2  #     3 ====== 2        |  1  |     |     4 === 3     |           |  #  
 |        |  3 === 2  #  2     |  3 ------ 3 --- 4 --- 5 === 3     |  1 ------ 4 --- 3 === 4  #  
 3 ------ 5 === 4 --- 5 ------ 4  #        |     |     |  1 ------ 4 ====== 2  |  3 --- 1  |  3  
 |        |     |     |  1     #  3 --- 2  |     2 --- 4 ====== 4 ------ 4 === 3  #        1  |  
 3 === 2  |     1     1  |     #        |  3 ====== 3 --- 1     |        |  1 --- 4 --- 2 --- 2  
    2 === 3        2 === 4 --- 5 ====== 4 --- 1        2 ====== 3        3 === 3 --- 3 === 2     

; END

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


Naoyuki Tamura
( Last modified: Sat Sep 27 00:07:41 2008 JST ,   ?????  Since June 4, 2008 )