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

はじめに

Nikoliによる ヤジリン(Yajilin)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます．

例題

Nikoliによる ヤジリンの例題 です．
例題
 ←
1		       
    →
0		    
      →
1		  
 ←
1		  2↓    
         
      →
1		  
         

ヤジリンのルール

Nikoliによるヤジリンのルールは以下の通りです．
(Rule 1)
盤面に線を引き，全体で1つの輪っかを作ります．
(Rule 2)
線はタテヨコにマスの中央を通り，1マスに1本だけ通過できます． 線は交差や枝分かれはしません．
(Rule 3)
線の通らないマスは黒マスになります．黒マスはタテヨコに連続しません． 数字のマスに線は通りませんが，黒マスにはなりません．
(Rule 4)
数字は矢印の方向に入る黒マスの数です．
ヤジリンを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます．

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

****************作成中****************

実行結果

すべての制約を記述したファイルを作成し， Sugarで実行すると以下のような結果が得られます． 
s SATISFIABLE
a x_0_0	1
a v_0_0	0
a h_0_0	0
a x_0_1	1
a v_0_1	0
a h_0_1	0
a x_0_2	0
a v_0_2	1
a h_0_2	-1
a x_0_3	0
a v_0_3	0
a h_0_3	-1
a x_0_4	0
a v_0_4	0
a h_0_4	-1
a x_0_5	0
a v_0_5	0
a h_0_5	-1
a x_0_6	0
a v_0_6	-1
a x_1_0	0
a v_1_0	1
a h_1_0	-1
a x_1_1	0
a v_1_1	0
a h_1_1	-1
a x_1_2	0
a v_1_2	0
a h_1_2	0
a x_1_3	1
a v_1_3	0
a h_1_3	0
a x_1_4	0
a v_1_4	-1
a h_1_4	1
a x_1_5	0
a v_1_5	0
a h_1_5	1
a x_1_6	0
a v_1_6	0
a x_2_0	0
a v_2_0	0
a h_2_0	1
a x_2_1	0
a v_2_1	0
a h_2_1	1
a x_2_2	0
a v_2_2	1
a h_2_2	0
a x_2_3	1
a v_2_3	0
a h_2_3	0
a x_2_4	0
a v_2_4	-1
a h_2_4	0
a x_2_5	1
a v_2_5	0
a h_2_5	0
a x_2_6	1
a v_2_6	0
a x_3_0	1
a v_3_0	0
a h_3_0	0
a x_3_1	1
a v_3_1	0
a h_3_1	0
a x_3_2	0
a v_3_2	1
a h_3_2	0
a x_3_3	1
a v_3_3	0
a h_3_3	0
a x_3_4	0
a v_3_4	-1
a h_3_4	0
a x_3_5	0
a v_3_5	1
a h_3_5	-1
a x_3_6	0
a v_3_6	-1
a x_4_0	0
a v_4_0	1
a h_4_0	-1
a x_4_1	0
a v_4_1	0
a h_4_1	-1
a x_4_2	0
a v_4_2	0
a h_4_2	0
a x_4_3	1
a v_4_3	0
a h_4_3	0
a x_4_4	0
a v_4_4	0
a h_4_4	-1
a x_4_5	0
a v_4_5	0
a h_4_5	0
a x_4_6	0
a v_4_6	-1
a x_5_0	0
a v_5_0	1
a h_5_0	0
a x_5_1	1
a v_5_1	0
a h_5_1	0
a x_5_2	0
a v_5_2	-1
a h_5_2	1
a x_5_3	0
a v_5_3	0
a h_5_3	1
a x_5_4	0
a v_5_4	1
a h_5_4	0
a x_5_5	1
a v_5_5	0
a h_5_5	0
a x_5_6	0
a v_5_6	-1
a x_6_0	0
a h_6_0	1
a x_6_1	0
a h_6_1	1
a x_6_2	0
a h_6_2	0
a x_6_3	1
a h_6_3	0
a x_6_4	0
a h_6_4	1
a x_6_5	0
a h_6_5	1
a x_6_6	0
a z_0_0	0
a r_0_0	0
a z_0_1	0
a r_0_1	0
a z_0_2	48
a r_0_2	0
a z_0_3	47
a r_0_3	0
a z_0_4	46
a r_0_4	0
a z_0_5	45
a r_0_5	0
a z_0_6	44
a r_0_6	0
a z_1_0	15
a r_1_0	0
a z_1_1	1
a r_1_1	1
a z_1_2	49
a r_1_2	0
a z_1_3	0
a r_1_3	0
a z_1_4	41
a r_1_4	0
a z_1_5	42
a r_1_5	0
a z_1_6	43
a r_1_6	0
a z_2_0	16
a r_2_0	0
a z_2_1	17
a r_2_1	0
a z_2_2	18
a r_2_2	0
a z_2_3	0
a r_2_3	0
a z_2_4	40
a r_2_4	0
a z_2_5	0
a r_2_5	0
a z_2_6	0
a r_2_6	0
a z_3_0	0
a r_3_0	0
a z_3_1	0
a r_3_1	0
a z_3_2	19
a r_3_2	0
a z_3_3	0
a r_3_3	0
a z_3_4	39
a r_3_4	0
a z_3_5	36
a r_3_5	0
a z_3_6	35
a r_3_6	0
a z_4_0	22
a r_4_0	0
a z_4_1	21
a r_4_1	0
a z_4_2	20
a r_4_2	0
a z_4_3	0
a r_4_3	0
a z_4_4	38
a r_4_4	0
a z_4_5	37
a r_4_5	0
a z_4_6	34
a r_4_6	0
a z_5_0	23
a r_5_0	0
a z_5_1	0
a r_5_1	0
a z_5_2	27
a r_5_2	0
a z_5_3	28
a r_5_3	0
a z_5_4	29
a r_5_4	0
a z_5_5	0
a r_5_5	0
a z_5_6	33
a r_5_6	0
a z_6_0	24
a r_6_0	0
a z_6_1	25
a r_6_1	0
a z_6_2	26
a r_6_2	0
a z_6_3	0
a r_6_3	0
a z_6_4	30
a r_6_4	0
a z_6_5	31
a r_6_5	0
a z_6_6	32
a r_6_6	0
a
Sugarの次期リリースには， 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です． 以下は，その実行例です． 
$ ./yajilin.pl data/yajilin-0.txt >csp/yajilin-0.csp

$ /usr/bin/time sugar csp/yajilin-0.csp >log/yajilin-0.log
3.19user 0.14system 0:02.19elapsed 151%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+624outputs (2major+15140minor)pagefaults 0swaps

$ ./yajilin.pl -s log/yajilin-0.log data/yajilin-0.txt
; Yajilin Puzzle
; # http://www.nikoli.co.jp/en/puzzles/yajilin/
; size 7 7
;   - L1  -  -  -  -  -
;   -  -  - R0  -  -  -
;   -  -  -  -  - R1  -
;   - L1  - D2  -  -  -
;   -  -  -  -  -  -  -
;   -  -  -  -  - L1  -
;   -  -  -  -  -  -  -

+   +   +   +   +   +   +   +
  #   L1  +---+---+---+---+  
+   +   + | +   +   +   + | +
  +---+---+   R0  +---+---+  
+ | +   +   +   + | +   +   +
  +---+---+   #   +   R1  #  
+   +   + | +   + | +   +   +
  #   L1  +   D2  +   +---+  
+   +   + | +   + | + | + | +
  +---+---+   #   +---+   +  
+ | +   +   +   +   +   + | +
  +   #   +---+---+   L1  +  
+ | +   + | +   + | +   + | +
  +---+---+   #   +---+---+  
+   +   +   +   +   +   +   +

; END

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

Naoyuki Tamura