スリザーリンク・パズルをSugar制約ソルバーで解く


はじめに

Nikoliによる スリザーリンク(スリリン, Slitherlink, Fences)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます.

例題

Nikoliによる スリザーリンクの例題 です.
例題
  0   1     1  
  3     2 3   2
    0         0
  3     0      
      3     0  
1         3    
3   1 3     3  
  0     3   3  

スリザーリンクのルール

Nikoliによるスリザーリンクのルールは以下の通りです.
(Rule 1)
点と点をタテヨコにつなげ,全体で1つの輪っかを作ります.
(Rule 2)
4つの点で作られた小さな正方形の中の数字は,その正方形の辺に引く線の数です. 数字のない小さな正方形の辺には,何本の線を引くかわかりません.
(Rule 3)
線は,交差したり枝分かれしたりはしません.
スリザーリンクを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

Rule 1

(Rule 1)
点と点をタテヨコにつなげ,全体で1つの輪っかを作ります.
実は,このRuleが一番難物です. 「全体で1つの輪っか」という条件は後回しにして, 複数の輪っかでも良いことにして話を進めます. 次に点とその隣の点を結ぶ辺(edge)に変数を割り当てます. これらの辺を表す変数は,辺を結ぶか結ばないかだけを表すのであれば, 0か1の値を取れば良いのですが,後述の処理のため, 辺の向きを含めて表現できるようにし,-1か0か1の値を取ることにします.

たとえば,左上の節点から下への辺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_i_j=1
の場合
v_i_j=0
の場合
v_i_j=-1
の場合
n_i_j
 
n_(i+1)_j

    n_i_j n_i_(j+1)
h_i_j=1の場合
h_i_j=0の場合
h_i_j=-1の場合

Rule 2

(Rule 2)
4つの点で作られた小さな正方形の中の数字は,その正方形の辺に引く線の数です. 数字のない小さな正方形の辺には,何本の線を引くかわかりません.
たとえば,4行目2列目には3が入っています. この回りの辺に対応する変数は,左がv_3_1,上がh_3_1, 右がv_3_2,下がh_4_1の4つです.

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)
他の数字のマスについても同様にします.

Rule 3

(Rule 3)
線は,交差したり枝分かれしたりはしません.
これは,線が輪っかを作る条件と合わせて考えると, すべての節点において, 結ばれている辺の個数(次数,degree)が0または2になるという条件で表すことができます.

そのため,まず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)
他の節点についても同様の条件を追加します.

Rule 1 再び

(Rule 1)
点と点をタテヨコにつなげ,全体で1つの輪っかを作ります.
ここまでで,「全体で1つの輪っか」という条件を除いて, 他の条件はすべて表現されています(辺の向きの条件も除いて良い).

ここまでは比較的簡単でしたが,「全体で1つの輪っか」という条件はかなり面倒です. 一つの方法は, できあがったグラフが連結(connected)であるという条件を追加することですが, 辺の個数の二乗に比例する制約条件が必要なように思われます. それだと,少し大きなパズルに対しては,制約条件の個数が膨大になり, 高速な制約ソルバーであるSugarでも解くことができません.

そこで,少し工夫をして, 以下のように辺の個数に比例する制約条件で表す方法を考えてみました. これより良い方法もあるかも知れません. ご存知の方は,著者までお知らせいただけましたら幸いです.

これまでの条件だと,複数の輪っかが存在する可能性があります. そこで,各輪っかについて,節点に1から順に番号を付けることにします. 番号は辺の向きにしたがって付けていきます. たとえば,二つの輪っかがある場合,以下のように各節点に番号を付けるのです.

1 2 3
6 5 4
3 2
4 1

左側の輪っかは左上の節点から順に辺の向きに番号が付けられており, 右側の輪っかは右下の節点から順に辺の向きに番号が付けられています.

このように節点に番号を付けることができれば, 「1の番号の付いた節点(始節点)がちょうど1つ」という条件により,輪っかを一つにできます.

「始節点がちょうど1つ」という条件は, 各節点について,その番号が1なら1の値を取り,それ以外の場合0の値を取る変数を用意し, すべての節点についてのそれらの合計が1に等しくなることで表現できます.

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

たとえば,節点n_1_2について,以下の宣言を加えます.
    (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で実行すると以下のような結果が得られます.

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

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


Naoyuki Tamura