・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
0 | 1 | 1 | ||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
3 | 2 | 3 | 2 | |||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
0 | 0 | |||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
3 | 0 | |||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
3 | 0 | |||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
1 | 3 | |||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
3 | 1 | 3 | 3 | |||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ||||||||
0 | 3 | 3 | ||||||||||||||
・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ | ・ |
たとえば,左上の節点から下への辺v_0_0および 右への辺h_0_0の宣言は以下のようになります.
(int v_0_0 -1 1) (int h_0_0 -1 1)他の辺を表す変数についても同様に宣言します.
変数v_i_j (あるいはh_i_j)が1の場合, 対応する辺が下向き (あるいは右向き)であることを表し, -1の場合,対応する辺が上向き (あるいは左向き)であることを表すものとします. これを,表にまとめると以下のようになります.
|
|
v_3_1の絶対値,すなわち(abs v_3_1)は,辺の向きにかかわらず, 辺が結ばれていれば1になります. したがって,回りにある線の数が3に等しいという条件は,以下のように記述できます.
(= (+ (abs v_3_1) (abs h_3_1) (abs v_3_2) (abs h_4_1)) 3)他の数字のマスについても同様にします.
そのため,まず0または2のみを値とするドメインdegreeを宣言します.
(domain degree (0 2)) ; degree = { 0, 2 }次に,各節点n_i_jに対し, その節点の次数を表す変数d_i_jを用意します. たとえば,節点n_1_2の次数を表す変数d_1_2を 以下のように宣言します.
(int d_1_2 degree) ; d_1_2 ∈ degree他の節点についても同様に宣言します.
節点n_1_2を一方の端点とする辺は, v_0_2, h_1_1, v_1_2, h_1_2の4つですから, 節点n_1_2の次数は以下のようにして計算できます.
(= d_1_2 (+ (abs v_0_2) (abs h_1_1) (abs v_1_2) (abs h_1_2)))他の節点についても同様に次数の条件を追加します.
次に,辺の向きについての条件を追加します. すなわち,できた輪っかの辺の向きがそろっているようにします. この条件は,各節点について,入ってくる辺の数と出て行く辺の数が一致することで 表現できます. たとえば,節点n_1_2についての条件は以下のようになります.
(= (+ v_0_2 h_1_1 (neg v_1_2) (neg h_1_2)) 0)他の節点についても同様の条件を追加します.
ここまでは比較的簡単でしたが,「全体で1つの輪っか」という条件はかなり面倒です. 一つの方法は, できあがったグラフが連結(connected)であるという条件を追加することですが, 辺の個数の二乗に比例する制約条件が必要なように思われます. それだと,少し大きなパズルに対しては,制約条件の個数が膨大になり, 高速な制約ソルバーであるSugarでも解くことができません.
そこで,少し工夫をして, 以下のように辺の個数に比例する制約条件で表す方法を考えてみました. これより良い方法もあるかも知れません. ご存知の方は,著者までお知らせいただけましたら幸いです.
これまでの条件だと,複数の輪っかが存在する可能性があります. そこで,各輪っかについて,節点に1から順に番号を付けることにします. 番号は辺の向きにしたがって付けていきます. たとえば,二つの輪っかがある場合,以下のように各節点に番号を付けるのです.
|
|
左側の輪っかは左上の節点から順に辺の向きに番号が付けられており, 右側の輪っかは右下の節点から順に辺の向きに番号が付けられています.
このように節点に番号を付けることができれば, 「1の番号の付いた節点(始節点)がちょうど1つ」という条件により,輪っかを一つにできます.
「始節点がちょうど1つ」という条件は, 各節点について,その番号が1なら1の値を取り,それ以外の場合0の値を取る変数を用意し, すべての節点についてのそれらの合計が1に等しくなることで表現できます.
そこで,まず以下の変数を用意します.
(int x_1_2 0 81) (int y_1_2 0 1)さらに, 次数d_1_2が正の時だけx_1_2が正になるという条件と, x_1_2が1に等しい時だけy_1_2が1に等しくなるという条件を 加えます.
(iff (> d_1_2 0) (> x_1_2 0)) (iff (= x_1_2 1) (= y_1_2 1))他の節点についても同様にします.
次に,すべてのy_i_jの和が1に等しいという条件を加え, 「始節点がちょうど1つ」すなわち「全体で1つの輪っか」という条件を表します.
(= (+ y_0_0 y_0_1 ... y_8_8) 1)最後は,つながっている辺への番号付けのための条件です.
たとえば,節点n_1_2から出る辺について考えます. v_0_2が負ならば, 節点n_1_2からn_0_2への辺があるので, 節点の番号x_0_2は,普通はx_1_2よりも一つ大きくなります. あるいは,節点n_0_2が始節点の場合もありえます. その場合x_0_2は1となります.
これを制約条件として書くと次のようになります (=>は論理記号の「ならば」を表します).
(=> (< v_0_2 0) (or (> x_0_2 x_1_2) (= x_0_2 1)))条件(> x_0_2 x_1_2)は, (= x_0_2 (+ x_1_2 1))のほうが上の説明に合致するのですが, 節点につける番号は必ずしも1ずつ増えなくても良いので, 単に大きいという条件で記述しています (このほうがSugar制約ソルバーに優しい(?)記述となるためです).
節点n_1_2から出る他の三つの辺についての制約条件を書くと 以下のようになります.
(=> (< h_1_1 0) (or (> x_1_1 x_1_2) (= x_1_1 1))) (=> (> v_1_2 0) (or (> x_2_2 x_1_2) (= x_2_2 1))) (=> (> h_1_2 0) (or (> x_1_3 x_1_2) (= x_1_3 1)))他の節点についても同様に記述します.
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です. 以下は,その実行例です.
$ ./slitherlink.pl data/slitherlink-0.txt >csp/slitherlink-0.csp $ /usr/bin/time sugar csp/slitherlink-0.csp >log/slitherlink-0.log 6.60user 0.16system 0:03.91elapsed 172%CPU (0avgtext+0avgdata 0maxresident)k 0inputs+1768outputs (2major+26342minor)pagefaults 0swaps $ ./slitherlink.pl -s log/slitherlink-0.log data/slitherlink-0.txt ; Slitherlink Puzzle ; # http://www.nikoli.co.jp/en/puzzles/slitherlink/ ; size 8 8 ; - 0 - 1 - - 1 - ; - 3 - - 2 3 - 2 ; - - 0 - - - - 0 ; - 3 - - 0 - - - ; - - - 3 - - 0 - ; 1 - - - - 3 - - ; 3 - 1 3 - - 3 - ; - 0 - - 3 - 3 - + + + + +---+---+---+---+ 0 1 | 1 | +---+ +---+ + +---+ +---+ | | 3 | | | 2 | 3 | | 2 + +---+ +---+ + +---+ + | 0 | 0 +---+---+ + + +---+---+ + 3 | 0 | +---+---+ +---+ + + +---+ | | 3 | 0 | + + +---+ + +---+ + + | 1 | | | 3 | | + +---+ +---+ + +---+ + | 3 | 1 | 3 | 3 | | +---+ + +---+ + +---+ + 0 | 3 | | 3 | + + + + +---+ +---+---+ ; END以下は, Nikoli: スリザーリンクのおためし問題中の おためし問題10 (36x20)をLet's Note CF-W5で解いた結果です(MiniSat2を使用). 7分半程度で解けています.
$ ./slitherlink.pl data/slitherlink-10.txt >csp/slitherlink-10.csp $ /usr/bin/time sugar csp/slitherlink-10.csp >log/slitherlink-10.log 444.52user 2.45system 7:21.10elapsed 101%CPU (0avgtext+0avgdata 0maxresident)k 48inputs+190456outputs (2major+102127minor)pagefaults 0swaps $ ./slitherlink.pl -s log/slitherlink-10.log data/slitherlink-10.txt ; Slitherlink Puzzle ; # http://www.nikoli.co.jp/en/puzzles/slitherlink/ ; size 36 20 ; - - - 3 - - - - 0 - 1 2 2 - - - - - - - - - - - 2 1 - 0 1 - - - - - 2 0 ; - 3 0 3 - 0 1 - - - - - - 3 3 2 1 - - 3 0 - 2 - - - - - - - - - - - - - ; - 3 - - - - - - 2 - - - - - - - - - - - - 3 - 3 - 3 - - 3 - - 3 - - 2 3 ; - 3 - - 3 - 0 - - - 0 - 3 - - 3 3 - - 3 - 2 - - - 0 1 - 3 - - 0 - - - - ; - 3 - 0 - - - 3 2 - 2 - 0 - - - - 3 - - - - - 3 - - - - 3 - - - 2 0 - 3 ; - - - - 3 2 - 3 - - 3 - 2 - - 2 2 - - - 0 - - - 1 3 - 1 - - 3 3 - - 3 - ; 1 3 1 - - - - - - - - 2 - 2 - - - - - - 3 - 1 - - - - 2 - - - - 1 - 2 - ; - - - - - 3 - 2 - 0 - - - 3 - 2 - - 3 - 2 - - 3 - - - - - - - - - - - - ; - - 3 0 - 3 - - 1 - 3 1 - - 3 - - - 0 - - - - 3 - 2 0 - 3 - 2 0 - - 3 1 ; 2 - - 3 - 2 - - - - - - 3 - - 2 - - 3 - - - - - - - - - 0 - - - - 0 - - ; - - 1 - - - - 2 - - - - - - - - - 2 - - 0 - - 2 - - - - - - 2 - 1 - - 1 ; 3 2 - - 0 3 - 2 - 3 3 - 2 - - - - 1 - - - 2 - - 2 2 - 3 - - 0 - 3 3 - - ; - - - - - - - - - - - - 0 - - 2 - 3 - - 2 - 2 - - - 3 - 3 - 1 - - - - - ; - 3 - 2 - - - - 3 - - - - 3 - 2 - - - - - - 0 - 2 - - - - - - - - 3 2 0 ; - 3 - - 2 1 - - 3 - 0 1 - - - 0 - - - 2 1 - - 2 - 3 - - 0 - 2 2 - - - - ; 2 - 0 3 - - - 1 - - - - 3 - - - - - 2 - - - - 1 - 0 - 1 2 - - - 3 - 2 - ; - - - - 2 - - 3 - 1 3 - - - 2 - 0 - - 2 0 - - 2 - 3 - - - 2 - 2 - - 3 - ; 1 3 - - 2 - - 3 - - 2 - 0 - 1 - - - - - - - - - - - - 3 - - - - - - 0 - ; - - - - - - - - - - - - - 3 - 3 3 - - 2 3 3 3 - - - - - - 3 3 - 3 3 3 - ; 1 0 - - - - - 0 1 - 2 1 - - - - - - - - - - - 1 0 1 - 1 - - - - 2 - - - +---+---+ +---+---+---+---+ + + + + +---+---+---+---+---+---+---+---+ + + +---+ + + + + +---+---+---+---+---+ + + | | | 3 | 0 1 2 | 2 | | | 2 1 0 1 | | 2 0 + +---+ +---+ + + +---+ +---+---+---+ +---+ +---+---+---+ +---+ + +---+ +---+---+---+ + + +---+---+---+ +---+ + | | 3 0 3 | 0 1 | | | 3 | 3 | 2 1 | | 3 0 | 2 | | | | | + +---+ +---+ + +---+ +---+ +---+---+---+ +---+ + + + +---+ +---+ +---+ +---+ + +---+ + +---+ +---+ +---+ | 3 | | | | 2 | | | | 3 | 3 | | 3 | | | 3 | | 3 | | 2 3 | + +---+ +---+ +---+ +---+---+---+ + +---+ +---+ +---+ + +---+ +---+ + +---+ +---+ +---+ +---+ +---+ +---+---+ | | 3 | 3 | 0 0 | 3 | | | 3 | 3 | | | 3 2 | | 0 1 3 | 0 | + +---+ + +---+ + +---+---+ + +---+ +---+ +---+ + + +---+---+ + +---+ + + + +---+ + + +---+ + +---+ | 3 | 0 | 3 2 | 2 | 0 | 3 | | | 3 | | 3 | 2 0 | 3 | + +---+ + +---+ + +---+ + +---+ + +---+---+---+ +---+ + + +---+ +---+ +---+ + +---+ +---+ + + +---+ + | | | 3 | 2 3 | | | 3 2 | 2 | 2 0 | 1 | 3 | 1 | | 3 | 3 | | 3 | + +---+ + + +---+---+---+ + +---+ +---+ +---+ +---+---+---+---+ +---+---+ + + +---+---+---+ + +---+ + +---+ + | 1 3 | 1 | | | 2 | 2 | | | 3 | 1 | 2 | 1 2 | | + +---+ +---+ +---+---+ +---+ + + + +---+ +---+---+ +---+ +---+ + +---+---+ +---+---+---+---+ +---+---+ + + + | | | | 3 | 2 | 0 | | | 3 2 | | 3 | 2 | 3 | | | | | + + +---+ + +---+ + + + +---+ + +---+ +---+ +---+ +---+---+---+ +---+ +---+ + +---+ +---+ + + +---+ + | | | 3 0 3 | | | 1 | 3 1 | | 3 | | 0 | 3 | | 2 0 | 3 | | 2 0 | | 3 1 | + + +---+ +---+---+ + + + +---+ +---+ +---+ + +---+ +---+---+ +---+---+ + + +---+ +---+ + +---+ +---+ + | 2 | | 3 | 2 | | | 3 | 2 | | | 3 | | | | 0 | 0 | | + +---+ +---+ +---+---+ + +---+---+ +---+ +---+---+ + +---+ + +---+---+ +---+ +---+ + + +---+---+ + +---+ + | | 1 | 2 | | | | | 2 0 | 2 | | | 2 1 | 1 | +---+ + + + +---+ +---+ + +---+ +---+ + +---+ +---+---+ + +---+---+ + +---+ +---+ +---+ + +---+ + + + 3 | 2 | 0 3 | | 2 | 3 | 3 | 2 | | | | 1 | | 2 | 2 | 2 | 3 | | 0 | 3 | 3 | | +---+ +---+---+ +---+ + + +---+ + + +---+ + +---+ +---+ +---+ +---+---+ + +---+ + + + +---+ +---+ +---+ | | | | | 0 | 2 | 3 | | 2 | 2 | | 3 | 3 | 1 | | + +---+---+ + +---+ +---+---+ + + + +---+ +---+ +---+ + + +---+ + +---+ +---+ +---+ + + +---+ +---+ + | | 3 | 2 | | 3 | | | 3 | 2 | | | 0 | 2 | | | | 3 | 2 0 + +---+ + +---+ +---+ +---+ + +---+---+ + + +---+ + +---+ +---+ +---+ +---+ + + + + + + +---+ + + | 3 | | 2 | 1 | | 3 0 1 | 0 | | 2 1 | | 2 | 3 | | 0 2 | 2 | + +---+ +---+ + +---+ +---+---+ + +---+---+ + +---+ +---+ +---+ +---+ +---+ +---+ + +---+---+ + +---+---+---+ | 2 | 0 3 | | | 1 | | 3 | | 2 | | 1 | 0 1 2 | | 3 | 2 | + + + +---+ + + +---+---+ +---+ +---+ + +---+ + + +---+ +---+---+ +---+ +---+---+---+ +---+ +---+ +---+ + | | | 2 | | | 3 | 1 3 | | 2 | 0 | | 2 0 | 2 | 3 | 2 | | 2 | 3 | | + +---+ + +---+ + +---+ + +---+ + +---+---+ + +---+ + + + + +---+ +---+ +---+---+---+ +---+---+---+ +---+ | 1 3 | | | 2 | 3 | | | 2 0 1 | | | | 3 0 + +---+ + + +---+ +---+ + + +---+ +---+ +---+ + +---+ +---+ +---+ +---+---+ +---+ +---+ +---+ +---+ +---+ | | | | | | | | | | | 3 | | 3 | 3 | | 2 | 3 | 3 | 3 | | | | 3 | 3 | | 3 | 3 | 3 | | +---+ + + +---+ +---+ + + +---+ +---+ +---+ +---+ +---+---+ +---+ + + + + + +---+ +---+ +---+ +---+ + 1 0 | | 0 1 | 2 1 | 1 0 1 | 1 2 | + + + +---+---+---+ + + +---+---+---+---+---+---+---+---+---+---+---+---+---+---+ + + +---+---+---+---+---+---+---+---+---+---+ ; END