コンパスおもしろいよね
ペンシルパズルを Sugar 制約ソルバー (SAT ソルバー) で解く企画第 2 弾。今回はコンパスを解きます。
ルール確認
トケタよりルール引用：
1. 点線に沿って線を引き、盤面をいくつかのブロックに分割します。
2. どのブロックにも、「コンパス」がちょうどひとつずつ入るようにします。コンパスのマスだけのブロックができてもかまいません。
3. コンパスの上側の数字は、そのコンパスは入るブロックｎ中で、コンパスよりも上にあるマスの数を表します。右、下、左についても同様です。
コンパスはルールにあるとおり分割系のパズルで、WPC や PGP など早解き界隈ではおなじみ。ルールの制約の絶妙な緩さ・厳しさにより、試行錯誤も必要となりかねない、難儀なパズルです。
一般に SAT ソルバーは分割系のパズルを解くのが苦手っぽいですが、どう対処しますかね。
困難は分割せよ
今回は、「マスがどのヒントに所属するか」を決めるものとします。ヒントにあらかじめ 0, 1, 2, ... と番号をふっておき、各マスの番号 x[i][j] を変数とします。この時点でかなり時間がヤバそうな予感...
制約を書く上でネックなのが、ブロックの連結性です。一般に連結性を扱うのは大変なので、一旦忘れることにしましょう。すると、残っているのはヒント数字の制約のみ。これは、ヒントマスから各方向のマスが何個かを数えるだけなので、Count 制約を使ってすぐに表せます。
というわけであとは連結性に帰着されました。連結性を扱うときの一般的な手法として、「全域木」を使うというものがあります。
ネック
ここでは一旦コンパスを離れて、別の例を考えてみます。
たとえば、へやわけのように白マスの連結性をチェックしたいとしましょう。各マスの変数 x[i][j] は黒マスかどうかで 0 か 1. 0 のマスが連結であってほしい ( = 分断してほしくない) です。
このとき、各マスに対応する新たな変数 z[i][j], r[i][j] を用意します。z はカウント用、r は「根」かどうかの判定用です。先ほど「全域木」と言いましたが、正確には「あるマスを根として、そこから隣接する白マスに辺を伸ばしていってつなげる」という操作をします。操作後、白マスすべてを使う全域木になっている、というわけですね。
SAT ではこういう操作を直接は行えないですが、制約の形で書くことはできます。それが z を用意した理由です。制約で書くときは、x の割り当てを考慮した上で
1. 黒マスと z = 0 が同値 (白マスは正)、根にもならない
2. 根のマスを z = 1 としておく
3. 根でない白マスの z について、隣接する白マスの z の値より大きい値を割り当てる
とします。そのような z と r の割り当てができれば全域木は完成です。さらに、全体の連結性を知りたいなら、根の個数を 1 個に制限しておくとよいです。連結成分が 2 個以上あるのに根が 1 つなら、根のない成分では 3. の制約が満たせません。
こんな感じで、変数を増やしてなんとか解決できます。実際にこの作戦で、へやわけの盤面に何個黒マスを詰められるかを検証したところ、マス数 50 個以下程度なら最大値を計算してくれました。
解決
本題に戻ります。今回の場合、ヒントのマスを根にすればよいです。
さっきと同じ変数 z を用意します (r は今回は不要)。そして、これも同様に x の割り当てを考慮した上で
1. 根のマス (= ヒントマス) は z = 0.
2. 根でないマスは、「同じ x の値で、かつ z が自分より小さい」マスが隣接している
という制約をおくとよいです。
なお、自分だけが孤立しないように注意が必要です。また、z の値の範囲は 0 から 盤面の個数未満とします。ロスが大きいですが仕方なさそうです。
書いて投げる
これで制約が作れたので、後は書くだけです。
例題としてこんな問題を作ってみました。実際に式を書き下して実行したところ、唯一解性を含めすぐに判定してくれました！やったね！！！
あとは自動化にむけて python でスクリプトを書いて、遊んでみました。
トケタの問題などを投げて遊んでいましたが、8×8 くらいなら高速で動いてくれるようです。また 12*12 の問題も 10 秒程度で解いてくれました。やったね！
比較的高速だったのは、 z の割り当てにあまり時間を取られていないから、が原因な気がします。また、根が既に確定しているのも大きいかもしれません。
今後の課題
・いつも通り、発見しづらい理詰めがある場合に低速になるかもしれない。実際、全体制約のある問題で速度が著しく低下した。制約追加で乗り切れるか。
・puzz.link のリンクを読み取って制約を自動で生成したいのですが、どうすればいいんでしょうね。
・今回の作戦は、ヒントがちょうど 1 つ入るタイプの分割系パズル (天体ショー) などに応用できそうで、汎用性高そう。Araf とか 2 つだとどうか。今後に期待。
