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


はじめに

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

例題

Nikoliによる ナンバーリンクの例題 です.
例題
  4     2
     1   
         
    5    
  1 3    
 52   3  
    4    

ナンバーリンクのルール

Nikoliによるナンバーリンクのルールは以下の通りです.
(Rule 1)
同じ数字どうしを線でつなげます.
(Rule 2)
線はタテヨコに引き,マスの中央を通ります.
(Rule 3)
線は1マスに1本だけ通過できます. 線をワクの外に出したり,交差や枝分かれさせてはいけません. また,線は数字が入っているマスを通過してもいけません.
ナンバーリンクを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

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

Rule 2

Rule 1は後回しにして,まずRule 2から考えます.
(Rule 2)
線はタテヨコに引き,マスの中央を通ります.
次にマス(節点)とその隣のマス(節点)を結ぶ辺(edge)に変数を割り当てます. これらの辺を表す変数は,辺を結ぶか結ばないを表すので, 0か1の値を取ります.

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

    (int v_0_0 0 1)
    (int h_0_0 0 1)
他の辺を表す変数についても同様に宣言します.

Rule 3

(Rule 3)
線は1マスに1本だけ通過できます. 線をワクの外に出したり,交差や枝分かれさせてはいけません. また,線は数字が入っているマスを通過してもいけません.
このRuleにより, 白マスから出ている(あるいは入っている)辺の個数(次数,degree)は 0または2となり, Rule 1と合わせて考えると数字のマスの次数は1となります.

そこで,白マスの次数を表すため, 0または2のみを値とするドメインdegreeを宣言します.

    (domain degree (0 2))  ; degree = { 0, 2 }
次に,各節点n_i_jに対し, その節点の次数を表す変数d_i_jを用意します. 節点が白マスの場合の値はドメインdegreeの値であり, 数字のマスの場合は1です.

たとえば, 白マスの節点n_0_1の次数を表す変数d_0_1 および数字のマスの節点n_0_2の次数を表す変数d_0_2の 宣言は以下のようになります.

    (int d_0_1 degree)
    (int d_0_2 1 1)
他の節点についても同様に宣言します.

次数を表す条件は,その節点を端点とする辺の値の合計となります.

たとえば,節点n_1_2を一方の端点とする辺は, v_0_2, h_1_1, v_1_2, h_1_2の4つですから, 節点n_1_2の次数は以下のようにして計算できます.

    (= d_1_2 (+ v_0_2 h_1_1 v_1_2 h_1_2))
他の節点についても同様に次数の条件を追加します.

「すべてのマスに辺がある」という条件を追加する場合は, ドメインdegreeの宣言を以下のように変更すればOKです.

    (domain degree 2 2)

Rule 1

(Rule 1)
同じ数字どうしを線でつなげます.
最後にRule 1について考えます. 線が同じ数字どうしをつないでいる条件を表すため, 各節点がどの数字とつながっているのかを表す変数を用います. 例題では,1から5の数字が現れていますから, 白マスの節点の変数x_i_jの値は,1から5のいずれかです.

たとえば,変数x_0_1x_0_2の 宣言は以下のようになります.

    (int x_0_1 1 5)
    (int x_0_2 4 4)
他の節点についても同様に宣言します.

次に,線でつながれている場合に, 変数x_i_jの値が同じになるという条件を追加します.

たとえば,辺v_0_2について考えます. この値が正の場合, 節点n_0_2と節点n_1_2は線でつながれているので, 変数x_0_2x_1_2の値は等しくなければいけません. これを,制約条件で記述すると以下のようになります (=>は論理記号の「ならば」を表します).

    (=> (> v_0_2 0) (= x_0_2 x_1_2))
他の辺についても同様に制約条件を追加します.

実行結果

すべての制約を記述したファイルを作成し, Sugarで実行すると以下のような結果が得られます.
s SATISFIABLE
a v_0_0	1
a h_0_0	1
a v_0_1	0
a h_0_1	1
a v_0_2	0
a h_0_2	1
a v_0_3	1
a h_0_3	0
a v_0_4	1
a h_0_4	1
a v_0_5	0
a h_0_5	0
a v_0_6	1
a v_1_0	1
a h_1_0	0
a v_1_1	1
a h_1_1	1
a v_1_2	0
a h_1_2	0
a v_1_3	1
a h_1_3	0
a v_1_4	1
a h_1_4	0
a v_1_5	1
a h_1_5	0
a v_1_6	1
a v_2_0	1
a h_2_0	0
a v_2_1	1
a h_2_1	0
a v_2_2	1
a h_2_2	1
a v_2_3	0
a h_2_3	0
a v_2_4	1
a h_2_4	0
a v_2_5	1
a h_2_5	0
a v_2_6	1
a v_3_0	1
a h_3_0	0
a v_3_1	1
a h_3_1	0
a v_3_2	1
a h_3_2	0
a v_3_3	1
a h_3_3	1
a v_3_4	0
a h_3_4	0
a v_3_5	1
a h_3_5	0
a v_3_6	1
a v_4_0	0
a h_4_0	0
a v_4_1	1
a h_4_1	0
a v_4_2	1
a h_4_2	0
a v_4_3	1
a h_4_3	0
a v_4_4	0
a h_4_4	1
a v_4_5	0
a h_4_5	0
a v_4_6	1
a v_5_0	1
a h_5_0	1
a v_5_1	0
a h_5_1	0
a v_5_2	0
a h_5_2	0
a v_5_3	0
a h_5_3	1
a v_5_4	0
a h_5_4	1
a v_5_5	0
a h_5_5	0
a v_5_6	1
a h_6_0	0
a h_6_1	1
a h_6_2	1
a h_6_3	1
a h_6_4	1
a h_6_5	1
a d_0_0	2
a d_0_1	2
a d_0_2	2
a d_0_3	2
a d_0_4	2
a d_0_5	1
a d_0_6	1
a d_1_0	2
a d_1_1	2
a d_1_2	1
a d_1_3	2
a d_1_4	2
a d_1_5	1
a d_1_6	2
a d_2_0	2
a d_2_1	2
a d_2_2	2
a d_2_3	2
a d_2_4	2
a d_2_5	2
a d_2_6	2
a d_3_0	2
a d_3_1	2
a d_3_2	2
a d_3_3	2
a d_3_4	2
a d_3_5	2
a d_3_6	2
a d_4_0	1
a d_4_1	2
a d_4_2	2
a d_4_3	2
a d_4_4	1
a d_4_5	2
a d_4_6	2
a d_5_0	2
a d_5_1	2
a d_5_2	1
a d_5_3	2
a d_5_4	2
a d_5_5	1
a d_5_6	2
a d_6_0	1
a d_6_1	1
a d_6_2	2
a d_6_3	2
a d_6_4	2
a d_6_5	2
a d_6_6	2
a x_0_0	2
a x_0_1	2
a x_0_2	2
a x_0_3	2
a x_0_4	3
a x_0_5	3
a x_0_6	4
a x_1_0	2
a x_1_1	1
a x_1_2	1
a x_1_3	2
a x_1_4	3
a x_1_5	5
a x_1_6	4
a x_2_0	2
a x_2_1	1
a x_2_2	2
a x_2_3	2
a x_2_4	3
a x_2_5	5
a x_2_6	4
a x_3_0	2
a x_3_1	1
a x_3_2	2
a x_3_3	3
a x_3_4	3
a x_3_5	5
a x_3_6	4
a x_4_0	2
a x_4_1	1
a x_4_2	2
a x_4_3	3
a x_4_4	5
a x_4_5	5
a x_4_6	4
a x_5_0	1
a x_5_1	1
a x_5_2	2
a x_5_3	3
a x_5_4	3
a x_5_5	3
a x_5_6	4
a x_6_0	1
a x_6_1	4
a x_6_2	4
a x_6_3	4
a x_6_4	4
a x_6_5	4
a x_6_6	4
a
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です. 以下は,その実行例です.
$ ./numberlink.pl data/numberlink-0.txt >csp/numberlink-0.csp

$ /usr/bin/time sugar csp/numberlink-0.csp >log/numberlink-0.log
1.08user 0.10system 0:00.93elapsed 126%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+176outputs (2major+10891minor)pagefaults 0swaps

$ ./numberlink.pl -s log/numberlink-0.log data/numberlink-0.txt
; Number Link Puzzle
; # http://www.nikoli.co.jp/en/puzzles/number_link/
; size 7 7
; - - - - - 3 4
; - - 1 - - 5 -
; - - - - - - -
; - - - - - - -
; 2 - - - 5 - -
; - - 2 - - 3 -
; 1 4 - - - - -

+   +   +   +   +   +   +   +
  +---+---+---+   +---3   4  
+ | +   +   + | + | +   + | +
  +   +---1   +   +   5   +  
+ | + | +   + | + | + | + | +
  +   +   +---+   +   +   +  
+ | + | + | +   + | + | + | +
  +   +   +   +---+   +   +  
+ | + | + | + | +   + | + | +
  2   +   +   +   5---+   +  
+   + | + | + | +   +   + | +
  +---+   2   +---+---3   +  
+ | +   +   +   +   +   + | +
  1   4---+---+---+---+---+  
+   +   +   +   +   +   +   +

; END

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


Naoyuki Tamura