ナンバーリンクをSATソルバーで解く

2022-01-04
昨日に引き続き、今度はナンバーリンクのソルバーを作ってみた。

ナンバーリンクとは?

ナンバーリンクもニコリの定番ペンシルパズルで、盤面に配置された同じ数字同士を線で結ぶというルール。 結構解き味が理詰めではなくて直感に頼らないと解けず、大きな盤面はお手上げという印象があるので個人的にはちと苦手…。

ナンバーリンクソルバー

前回と同様にSATソルバーのLogic Solverモジュールを利用する。 ナンバーリンクでは線を引いて、同じ数字同士がちゃんとつながっているかという判定をどうするかがキモとなる。

隣り合うマスに横線または縦線を引くかどうかの真偽値を変数にする。 そして線はつながるので、それぞれのマスに対して関係する4本のうちの2本が真となる (0ということも配置によってはあり得るがニコリの問題では必ず盤面を埋め尽くすためひとまず考えない)。 例外で数字が入っているマスからは線が1本しか出ない。

数字の連結判定

同じ数字同士が結ばれているかどうかを判定するには、各マスごとに variableBits の変数を用意する。 数字の入っているマスは当然その値、そして線で結ばれているマス同士は同じ数値が入る、という条件を指定することで違う数字同士が結ばれた場合には条件を満たさないため弾かれるようになる。

「線がつながってたら同じ数値になる」という条件を指定するには、「〜ならば(→)」を表す Logic.implies が使える。

追加の条件

本来は上記のルールだけで足りているがそれだけだと条件が緩いのか、解くのにかなり時間がかかってしまい、場合によってはメモリ不足で求まらない。 なのでルールから導かれる規則を足してやる。

線が「コ」の字の形は明らかに無駄でショートカットできるので、そのような経路はないという制約を追加してやる (線が入らないマスはないということが前提になっている)。

結果

以上で広い盤面でも1秒未満程度で解けるソルバーができた。 ただし解答が盤面をすべて埋め尽くすということが前提となっている。 線が通らずに残る空白のマスもありえる、とすると(下記ソースの36行目あたり)なかなか解が求まらずにメモリ不足で終了してしまったりする。 その対処法はわからなかった…。

マスを通る線が2本という判定に sum を使ってたのが無駄なんじゃないかと展開してみたりしたけど変わらず。

ソース

参考