スリザーリンクをSATで解いてみる

SATソルバーを使っていろんなパズルを解いたりしているのですが、今度はスリザーリンクのソルバーを作ってみました。

パズルのルール

発祥元であるニコリ社のサイトを見てもらってもいいのですが、こちらにも書いておきます。

1. 盤面の点をタテヨコに結んで、全体で1つの輪っかにする。
2. 数字のあるマスについては、周囲4辺のうちその数字の本数だけ線が通る。
3. 線は分岐したり交差したりはしない。

先行事例

Sugarという、制約充足問題（true/falseだけでなく、整数など変数が一定の範囲を取れるようになった充足問題）をSATに変換して解くソルバーがあるのですが、それを使ってスリザーリンクを解く例も用意してありました。

ただ、この方法では「0〜辺の数」まで取る変数を用意しているので、手でSATに書き直すには規模が大きすぎます。ということで、別なアプローチでSATを立ててみることにします。

できること・できないこと

まずは、「全体がつながっている」という条件についてはSATで求めず、JavaScript側で判定することにしました。というのも、CSPでないSATでこの条件を起こすのも面倒で、なおかつ「分離していたら解き直し」としてもそれなりに高速で解けることがわかったからです。

定式化の方針

手でスリザーリンクを解くときにも使われる手法ですが、ジョルダンの閉曲線定理より、分岐も交差もせず1つの輪っかとなっているスリザーリンクの答えのラインは、盤面を「外側」と「内側」に二分することとなります¹。ということで、盤面を「内側」と「外側」に塗り分ける問題として、スリザーリンクを再解釈してみます。

1. 以下のルールに従って、盤面の一部のマスに色を塗る。
2. マスに入った数字は、隣接する4マス（枠の外側も隣接すると考える）のうち、そのマスと違う色になるマスの数を表す。
3. 盤面から取った2マス×2マスのブロックについて、クロスするような形で2マスずつ色違いになることはない。
4. 同じ色のマスは分断しない。
5. 色を塗ったマスは、すべてタテヨコにひとつながりとなっている。
6. 色を塗っていないマスは、タテヨコにたどっていくとすべて外側につながる。

このうち、最後2項目はSAT化するのが難しいので、残る2項目を考えてみます。なお、盤面の「外側」という概念が入ってくる都合上、上下左右に1マスずつ広げて、番兵となる白マスを入れた状態で考えます。

変数としては、各マスが内側になるか、というものが、番兵分も入れて必要となります。

2×2のブロック

これは比較的簡単で、例えば $a_1$、$a_2$、$b_1$、$b_2$ というように4マスが並んでいたとすれば、そのまま論理式に起こして、

(\neg a_1 \vee a_2 \vee b_1 \vee \neg b_2)\wedge(a_1 \vee \neg a_2 \vee \neg b_1 \vee b_2)

というように書くだけです。なお、外側では番兵が並んでいる以上、この形は起き得ないので不要です。

数字のあるマス

以降、注目するマスを $c$、それに隣接する4マスを $n_1\dots n_4$ のように書きます（盤面に方向性はないので、4方向のどれをどれに対応させても構いません）。

まず、「1マスだけ孤立する」というのを防止するために、数字があってもなくても $\neg c \vee n_1 \vee n_2 \vee n_3 \vee n_4$ と $c \vee \neg n_1 \vee \neg n_2 \vee \neg n_3 \vee \neg n_4$ の2条件を追加しておきます（もちろん理屈の上では、「その1マスだけにループが発生する」という問題を考えることはできますが、基本的に自明な解にしかならないので考慮からは除外します）。

それでは数字の入っている場合を考えます。入っている数字が3の場合、「同じ色になるものは周囲4つの中で1つしかない」ということなので、6通りの組み合わせで $n_1\dots n_4$ から $n_i$、$n_j$ を抽出して、$(c \vee n_i \vee n_j)\wedge(\neg c \vee \neg n_i \vee \neg n_j)$ の条件を立てればOKです。

数字が2の場合、このマスの色にかかわらず、周囲4マスのうち色が付くのは2マスです。ということで、「3マスが同じ色になることはない」という条件を4つかければ大丈夫です。

数字が1の場合、ちょうど3の時の正反対で、$(c \vee\neg n_i \vee\neg n_j)\wedge(c \vee \neg n_i \vee \neg n_j)$ とすればよさそうですが、これでは「全部同じになる」パターンも通してしまいます。$n_1 \vee n_2 \vee n_3 \vee n_4$ と$\neg n_1 \vee \neg n_2 \vee \neg n_3 \vee \neg n_4$ という条件でそのパターンも消しておきます。

数字が0の場合、エレガントな書き方があります。

(c \vee\neg n_1)\wedge(n_1 \vee\neg n_2)\wedge(n_2 \vee\neg n_3)\wedge(n_3 \vee\neg n_4)\wedge(n_4 \vee\neg c)

実際に $c$へtrue/falseを入れてみれば、すべて等しくなることがわかると思います。

ループ削減

SATの外側で行うのですが、ループが分断しているものは解とならないので除外する必要があります。まず、「このループが不要」という場合、ループの辺に隣接するマスすべて（=孤立したマスと、そこに隣接するマス）について、元の条件を否定したものでORをとって条件に追加します。

まず、白マスの分断がある場合は簡単で、外側に繋がらないものはすべて除去すべきループです。

一方、色付きのマスの場合、「本来の解答＋余計なループ」というパターンになる可能性が、少ないながらもあります。ということで、ループに隣接する、0位外の数字の数を数えておいて、もしすべての数字がそのループに絡むなら除去しない、というような判定をする必要があります。

実際に作ってみて

意外と表示部分で手こずったりもしました。

1. 実は、ジョルダンの閉曲線定理は「平面上にある分岐も交差もしない閉曲線は、平面を内側と外側に二分する」というだけの内容です。数学者でもない身としては、そもそも証明すべき事実だと受け取ることも難しいですし、ましてやどうやって証明したものか見当もつきません。 ↩