お絵かきロジックをSugar制約ソルバーで解く


はじめに

お絵かきロジック(ののぐらむ, イラストロジック, ピクロス, Nonogram)パズルを Sugar制約ソルバー (A SAT-based Constraint Solver)で解いてみます. Copris上のノノグラムソルバー もご覧ください.

例題

Wikipediaによる お絵かきロジックの例題です.
例題

21 12
11 1132
4621 1221
         
2 2           
2 2           
         
         
2 2           
2 2           
         

お絵かきロジックのルール

お絵かきロジックのルールは以下の通りです.
(Rule 1)
以下のルールに従って盤面をぬりつぶします.
(Rule 2)
数字は,その行または列で連続に塗りつぶす黒マスのブロックの長さを表します.
(Rule 3)
数字が複数ある場合,黒マスのブロックはその順序に並びます. また,黒マスのブロックどうしの間は1マス以上空いていなければなりません.
お絵かきロジックを 制約充足問題(CSP, Constraint Satisfaction Problem)として表すための 方法について考えていきます.

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

Rule 1

(Rule 1)
以下のルールに従って盤面をぬりつぶします.
Ruleに従い,次のようにします. 変数x_0_0は,0か1の値のいずれかを取るので,以下のように宣言します.
    (int x_0_0 0 1)  ; 0行目0列目は0か1のいずれかの値が入る
他の変数も同様に宣言します.

Rule 2

(Rule 2)
数字は,その行または列で連続に塗りつぶす黒マスのブロックの長さを表します.

0行目には長さ4のブロックがあります.

このブロックの位置を変数で表すことにします. 変数h_0_0を用意し, この変数でブロックの左端の位置(列の番号)を表します. また,ブロックが盤面の中に入らないといけないので, h_0_0の上限値を,行の幅からブロックの長さを引いた4とします.

    (int h_0_0 0 4)

この時,j 列目のマスx_0_jが塗りつぶされるのは, j の値がh_0_0以上h_0_0+4未満の場合です. そこで,各j に対しての制約条件は以下のようになります.

    (iff (= x_0_j 1) (and (<= h_0_0 j) (< j (+ h_0_0 4))))
ここで,iffはif-and-only-if (その時,かつその時に限る)という意味で, 二つの論理式が同値であることを表します. すなわち右側の論理式は,黒マスになる必要条件を与えているだけでなく十分条件も与えており, 右側の論理式を満たさない場合には白マスになることも表しています.

しかし,各j に対して同様の制約条件を記述するのは面倒です. 以下のようにr_0という述語(predicate)を定義して,記述すれば簡単です.

    (predicate (r_0 j) (and (<= h_0_0 j) (< j (+ h_0_0 4))))
    (iff (= x_0_0 1) (r_0 0))
    (iff (= x_0_1 1) (r_0 1))
    (iff (= x_0_2 1) (r_0 2))
    (iff (= x_0_3 1) (r_0 3))
    (iff (= x_0_4 1) (r_0 4))
    (iff (= x_0_5 1) (r_0 5))
    (iff (= x_0_6 1) (r_0 6))
    (iff (= x_0_7 1) (r_0 7))

次に,1行目には長さ2のブロックが2つあります. 1つ目(左側)のブロックの左端の位置をh_1_0で表し, 2つ目(右側)のブロックの左端の位置をh_1_1で表すことにします.

    (int h_1_0 0 6)
    (int h_1_1 0 6)

この時,j 列目のマスx_1_jが塗りつぶされるのは, j の値がh_1_0以上h_1_0+2未満の場合, あるいはh_1_1以上h_1_1+2未満の場合です. そこで,j 列目が黒になる条件を表す述語を定義します.

    (predicate (r_1 j) (or (and (<= h_1_0 j) (< j (+ h_1_0 2)))
                           (and (<= h_1_1 j) (< j (+ h_1_1 2)))))
すると,各j に対する制約条件は以下のようになります. そこで,各j に対して,以下の制約条件を追加します.
    (iff (= x_1_0 1) (r_1 0))
    (iff (= x_1_1 1) (r_1 1))
    (iff (= x_1_2 1) (r_1 2))
    .....
    (iff (= x_1_7 1) (r_1 7))

他の行についても同様に制約条件を記述します.

各列の数字についても同様に考えます.

たとえば,2列目には上から順に長さ2, 1, 2の3つのブロックがあります. それぞれのブロックの上端の位置(行番号)を 変数v_2_0, v_2_1, v_2_2で表します.

    (int v_2_0 0 6)
    (int v_2_1 0 7)
    (int v_2_2 0 6)

この時,i 行目のマスx_i_2が塗りつぶされる条件を表す述語は 以下のように定義できます.

    (predicate (c_2 i) (or (and (<= v_2_0 i) (< i (+ v_2_0 2)))
                           (and (<= v_2_1 i) (< i (+ v_2_1 1)))
                           (and (<= v_2_2 i) (< i (+ v_2_2 2)))))
そこで,各i に対して,以下の制約条件を追加します.
    (iff (= x_0_2 1) (c_2 0))
    (iff (= x_1_2 1) (c_2 1))
    (iff (= x_2_2 1) (c_2 2))
    .....
    (iff (= x_7_2 1) (c_2 7))

他の列についても同様に制約条件を記述します.

Rule 3

(Rule 3)
数字が複数ある場合,黒マスのブロックはその順序に並びます. また,黒マスのブロックどうしの間は1マス以上空いていなければなりません.
1行目について, このRuleは以下の制約条件として記述できます.
    (< (+ h_1_0 2) h_1_1)

他の行,列についても同様に記述します.

実行結果

すべての制約を記述したファイルを作成し, Sugarで実行すると以下のような結果が得られます.
s SATISFIABLE
a x_0_0	0
a x_0_1	0
a x_0_2	1
a x_0_3	1
a x_0_4	1
a x_0_5	1
a x_0_6	0
a x_0_7	0
a x_1_0	0
a x_1_1	1
a x_1_2	1
a x_1_3	0
a x_1_4	0
a x_1_5	1
a x_1_6	1
a x_1_7	0
a x_2_0	1
a x_2_1	1
a x_2_2	0
a x_2_3	0
a x_2_4	0
a x_2_5	0
a x_2_6	1
a x_2_7	1
a x_3_0	1
a x_3_1	1
a x_3_2	1
a x_3_3	1
a x_3_4	1
a x_3_5	1
a x_3_6	1
a x_3_7	1
a x_4_0	1
a x_4_1	1
a x_4_2	0
a x_4_3	0
a x_4_4	0
a x_4_5	0
a x_4_6	0
a x_4_7	0
a x_5_0	1
a x_5_1	1
a x_5_2	0
a x_5_3	0
a x_5_4	0
a x_5_5	0
a x_5_6	1
a x_5_7	1
a x_6_0	0
a x_6_1	1
a x_6_2	1
a x_6_3	0
a x_6_4	0
a x_6_5	1
a x_6_6	1
a x_6_7	0
a x_7_0	0
a x_7_1	0
a x_7_2	1
a x_7_3	1
a x_7_4	1
a x_7_5	1
a x_7_6	0
a x_7_7	0
a h_0_0	2
a h_1_0	1
a h_1_1	5
a h_2_0	0
a h_2_1	6
a h_3_0	0
a h_4_0	0
a h_5_0	0
a h_5_1	6
a h_6_0	1
a h_6_1	5
a h_7_0	2
a v_0_0	2
a v_1_0	1
a v_2_0	0
a v_2_1	3
a v_2_2	6
a v_3_0	0
a v_3_1	3
a v_3_2	7
a v_4_0	0
a v_4_1	3
a v_4_2	7
a v_5_0	0
a v_5_1	3
a v_5_2	6
a v_6_0	1
a v_6_1	5
a v_7_0	2
a v_7_1	5
a
Sugarの次期リリースには, 問題ファイルを読み込んで 制約条件を記述したCSPファイルを作成するツールを含める予定です. 以下は,その実行例です.
$ ./nonogram.pl data/nonogram-0.txt >csp/nonogram-0.csp

$ /usr/bin/time sugar csp/nonogram-0.csp >log/nonogram-0.log
1.36user 0.08system 0:01.18elapsed 122%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+160outputs (2major+12062minor)pagefaults 0swaps

$ ./nonogram.pl -s log/nonogram-0.log data/nonogram-0.txt
; Nonogram Puzzle
; # http://ja.wikipedia.org/wiki/%E3%81%8A%E7%B5%B5%E3%81%8B%E3%81%8D%E3%83%AD%E3%82%B8%E3%83%83%E3%82%AF
; size 8 8
; R 0	4
; R 1	2 2
; R 2	2 2
; R 3	8
; R 4	2
; R 5	2 2
; R 6	2 2
; R 7	4
; C 0	4
; C 1	6
; C 2	2 1 2
; C 3	1 1 1
; C 4	1 1 1
; C 5	2 1 2
; C 6	3 2
; C 7	2 1

. . # # # # . . 
. # # . . # # . 
# # . . . . # # 
# # # # # # # # 
# # . . . . . . 
# # . . . . # # 
. # # . . # # . 
. . # # # # . . 

; END

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


Naoyuki Tamura