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


はじめに

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

例題

Nikoliによる カックロの例題 です. 斜線が入っていませんが,ご容赦ください.
例題
    11   4      
  14 5     10    
  17         3  
  6     3 4    
    10        
      3      

カックロのルール

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行目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

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


Naoyuki Tamura
( Last modified: Fri Jun 27 14:44:22 2008 JST ,   ?????  Since June 4, 2008 )