カックロ・パズルをSugar制約ソルバーで解く

はじめに

Nikoliによるカックロ(Kakuro, クロスサム, Cross Sums)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます．

例題

Nikoliによるカックロの例題です．斜線が入っていませんが，ご容赦ください．例題

		₁₁	₄
	₁₄ ⁵			₁₀
¹⁷					₃
⁶			₃ ⁴
	¹⁰
		³

カックロのルール

Nikoliによるカックロのルールは以下の通りです．

(Rule 1): あいているマスに，1から9までの数字のどれかを入れます．0(ゼロ)は使いません．
(Rule 2): ナナメの線の右上に出ている数字は，その右の白マスのつながりに入る数字の合計．ナナメの線の左下に出ている数字は，その下の白マスのつながりに入る数字の合計です．
(Rule 3): タテヨコへの1つの白マスのつながりには，同じ数字は入りません．

カックロを制約充足問題(CSP, Constraint Satisfaction Problem)として表すための方法について考えていきます．

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

Rule 1

(Rule 1): あいているマスに，1から9までの数字のどれかを入れます．0(ゼロ)は使いません．

Ruleに従い，次のようにします．

各白マスに1から9の値を取る変数を割り当てて，入れる数字を表すことにします．
i 行目，j 列目のマスに変数x_i_jを割り当てます．
白でないマスには変数を割り当てません．

たとえば，1行目2列目(11の数字の下)は白マスなので，変数x_1_2を割り当て，以下のように宣言します．

    (int x_1_2 1 9)  ; 2行目3列目には1から9のいずれかの値が入る

他の変数も同様に宣言します．

Rule 2

(Rule 2): ナナメの線の右上に出ている数字は，その右の白マスのつながりに入る数字の合計．ナナメの線の左下に出ている数字は，その下の白マスのつながりに入る数字の合計です．

たとえば， 1行目1列目の左下には14が入っています．これは，x_2_1, x_3_1の合計が14に等しいという条件を表しています．また， 1行目1列目の右上には5が入っています．これは，x_1_2, x_1_3の合計が5に等しいという条件を表しています．これらの条件は，以下のように記述できます．

    (= (+ x_2_1 x_3_1) 14)
    (= (+ x_1_2 x_1_3) 5)

他の数字のマスについても同様にします．

Rule 3

(Rule 3): タテヨコへの1つの白マスのつながりには，同じ数字は入りません．

たとえば，2行目1列目から4列目までのつながりには，同じ数字は入りません．すなわち，x_2_1, x_2_2, x_2_3, x_2_4がすべて互いに異なるということです．この条件は， allDifferent制約を用いて以下のように表現できます．

    (allDifferent x_2_1 x_2_2 x_2_3 x_2_4)

他の白マスのつながりについても同様にします．

注意: Sugar version 1.13では，allDifferent ではなく alldifferent と小文字で書いてください．

実行結果

すべての制約を記述したファイルを作成し， Sugarで実行すると以下のような結果が得られます．

s SATISFIABLE
a x_1_2	2
a x_1_3	3
a x_2_1	9
a x_2_2	5
a x_2_3	1
a x_2_4	2
a x_3_1	5
a x_3_2	1
a x_3_4	3
a x_3_5	1
a x_4_2	3
a x_4_3	1
a x_4_4	4
a x_4_5	2
a x_5_3	2
a x_5_4	1
a

Sugarの次期リリースには，問題ファイルを読み込んで制約条件を記述したCSPファイルを作成するツールを含める予定です．以下は，その実行例です．

$ ./kakuro.pl data/kakuro-0.txt >csp/kakuro-0.csp

$ /usr/bin/time sugar csp/kakuro-0.csp >log/kakuro-0.log
0.64user 0.09system 0:00.72elapsed 101%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+160outputs (2major+8883minor)pagefaults 0swaps

$ ./kakuro.pl -s log/kakuro-0.log data/kakuro-0.txt
; Kakuro Puzzle
; # http://www.nikoli.co.jp/en/puzzles/kakuro/
; size 6 6
;  0\0   0\0  11\0   4\0   0\0   0\0
;  0\0  14\5    -     -   10\0   0\0
;  0\17   -     -     -     -    3\0
;  0\6    -     -    3\4    -     -
;  0\0   0\10   -     -     -     -
;  0\0   0\0   0\3    -     -    0\0

[ 0\ 0][ 0\ 0][11\ 0][ 4\ 0][ 0\ 0][ 0\ 0]
[ 0\ 0][14\ 5]   2      3   [10\ 0][ 0\ 0]
[ 0\17]   9      5      1      2   [ 3\ 0]
[ 0\ 6]   5      1   [ 3\ 4]   3      1
[ 0\ 0][ 0\10]   3      1      4      2
[ 0\ 0][ 0\ 0][ 0\ 3]   2      1   [ 0\ 0]

; END

Kakuro Solver in Copris も参照してください．

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

Naoyuki Tamura