ペンシルパズルを自作して、唯一解判定ソルバーをSugar CSPソルバで作る

このペンシルパズルのルール

• すべてのマスに道を引く。

• 道は枝分かれや交差をしない。

• 手がかりの位置は道の始点のマスをすべて表す。

• すべての道は始点から右折だけを行って伸びる。

• 手がかりの数字はその道の右折の回数を表す。

ペンシルパズル問題は唯ー解でなくてはならない

制約ソルバーSugarにペンシルパズルを解かせる

Sugarは与えられた制約を満たす解を見つける

(int x 0 1)
(int y 0 1)
(= (+ x y) 1)

• 1、2行目は変数定義です。変数$x,y\in \{a | 0 \le a \le 1, a \in \mathbb{Z}\}$を定義しています。

• 3行目は制約定義です。$x+y=1$です。

ペンシルパズルをSugarの制約に変換する

各マスがそれぞれ持つ変数情報

• Area: 通る道の手がかり番号 (1〜手がかりの数) ※手がかりごとに独立の番号をふる。

• Type: 直線か右折か始点か終点か (0直線、1右折、2始点、3終点)

• PathY: 下へ道があるか (-1逆向き、0なし、1順向き) ※道は向きがあるとする。

• PathX: 右へ道があるか(-1逆向き、0なし、1順向き)

• Order: 始点を1として道に連番を降ったときの数字 (1-全マス数)

(制約StartPath) Type=始点は1本だけ道が始まる

• Type=始点か終点ならば、次のうち1が1つだけ、ほかの3つは0。
• 「このマスのPathX」
• -1 ×「左のマスのPathX」
• 「このマスのPathY」
• -1 ×「上のマスのPathY」

(制約EndPath) Type=終点は1本だけ道が終わる

(制約Straight) Type=直進ならば道は直進

• Type=直進のマスは次のどちらかを満たす;
• 「このマスのPathX」×「左のマスのPathX」= 1
• 「このマスのPathY」×「上のマスのPathY」= 1

(制約TurnRIght) Type=右折ならば道は右折

• Type=右折のマスはPathXとPathYがいい感じに右折

(制約StartHint) 始点は手がかりのあるところのみ

• マスに手がかりがあるならば、Area=手がかり番号、Type=始点

• なければ、Type≠始点

(制約Area) 道があるならば同じAreaに属する

• PathX≠0ならば、「このマスのArea」=「右のマスのArea」

• PathY≠0ならば、「このマスのArea」=「下のマスのArea」

(制約End) Areaごとに終点は1つ

• すべての手がかり番号Nについて、「Area=NかつType=終点となる変数」の個数=1

(制約NumberHint) Areaごとに手がかりの数だけ右折

• すべての手がかり番号Nについて、「Area=NかつType=右折となる変数」の個数=手がかり番号Nの数字

これらの制約で十分でしょうか?

(制約NoLoop) 道に沿って1から順番に数字を振ることができる

• Type=始点

• PathX=1ならば、「このマスのOrder」+ 1 =「右のマスのOrder」

• PathX=-1ならば、「このマスのOrder」- 1 =「右のマスのOrder」

• PathY=1ならば、「このマスのOrder」+ 1 =「下のマスのOrder」

• PathY=-1ならば、「このマスのOrder」- 1 =「下のマスのOrder」

出来た制約をSugarに投げる

typhoon-puzzle/puzzle/small.txt.csp at master · wass88/typhoon-puzzle

Contribute to wass88/typhoon-puzzle development by creating an account on GitHub.

https://github.com/wass88/typhoon-puzzle/blob/master/puzzle/small.txt.csp

s SATISFIABLE
; Size 4x4
;# Area variables
; 3 3 1 2
; 3 3 1 2
; 2 1 1 2
; 2 2 2 2
;# Type variables
; 1 1 2 2
; 2 3 0 0
; 3 3 1 0
; 1 0 0 1
;# Path variables
; +--+  +  +
; !  |  |  |  
; +  +  +  +
;       |  |  
; +  +~~+  +
; !        |  
; +~~+~~+~~+

解を除外して唯一解判定をする

s UNSATISFIABLE

参考文献

• パズルをSugar制約ソルバーで解く(Naoyuki Tamura)