（この記事は、連載記事です。ソルバー自体その1）

「ナンバーリンクを、SATとして解く」という方針が決まれば、あとの課題は「ナンバーリンクをSATに変換する」ことと「SATソルバーを動かす」ことの2つに分けられます。今回は、前者の「ナンバーリンクをSATに変換する」部分について解説していきます。

まず、よく使う道具の用意

ナンバーリンクを論理式化する上で、「これらの4つの変数の中でtrueになるのは2つ以下」のようなパターンが多数登場します。まずは、そのパターンをCNFに書き下してみることにします。

シンプルな「falseが○個以下」

まず、「変数が $n$ 個ある中で、falseを取るのは $k$ 個以下」、というパターンについて考えてみます（もちろん、$n>k$ でなければ自明です）。

変数の中にfalseは $k$ 個以下しかないわけですから、元の変数から $k+1$ 個取ってきてORを取れば、これは（どんなパターンで $k+1$ 個を取ってきたとしても）必ずtrueになります。逆に、$k+1$ 個取ってORしたパターンを全部網羅してANDしておけば、もし $k+1$ 個以上のfalseがあった場合には、$k+1$ 個だけORしたもののうち少なくともどれか1つで、すべての変数がfalseになり、OR節自体もfalseとなります。

そして、SATの変数はtrueかfalseしか取りませんので、「変数が $n$ 個ある中で、falseを取るのは $k$ 個以下」ということはすなわち「変数が $n$ 個ある中で、trueを取るのは $n-k$ 個以上」と同値です。

「trueが○個以下」、「ちょうど○個」

逆に「変数が $n$ 個ある中で、trueを取るのは $k$ 個以下」という条件を考える場合は、同様に元の変数から $k+1$ 個取ってきて、全てにNOTをかけた上でORをかけたものを、全パターンについてANDをとれば表現できます。そして、「ちょうど $k$ 個」ということを表現したい場合、「 $k$ 個以上かつ $k$ 個以下」なので、両方についてANDを取れば表現できます。

具体例として、$A$、$B$、$C$、$D$という4つの変数について、「trueが2つ以下」という場合は、

(\neg A\vee\neg B\vee\neg C)\wedge(\neg A\vee\neg B\vee\neg D)\wedge(\neg A\vee\neg C\vee\neg D)\wedge(\neg B\vee\neg C\vee\neg D)

のようになります。

ナンバーリンクのルールを変形する

正しく考えれば、各マスに「線」を入れることを考えないといけないのですが、それをするとなると通る線の形と、線が結んでいる数字との両方を考えないといけなくなって、少々面倒です。そこで、線の代わりに盤面を「数字」で埋めることにします。すると、ルールは

次のルールに従って、盤面に1つずつ数字を入れます。
もともと盤面に入っていた数字2つが、同じ数字をタテヨコにたどってつながるようにします。
もともと盤面に入っていた数字については、タテヨコに隣接するマスのうち1つだけに同じ数字が入ります。
空きマスに入れる数字については、タテヨコに隣接するマスのうちちょうど2つに同じ数字が入ります。

のように変換できます。

変形の代償

ただし、3・4については注意が必要です。引きだした線が曲がって、さっき引いた線の隣に来てしまうと、数字に変換した時に3や4の条件を満たさなくなることがあります。他のパズルであれば解けなくなってしまうのですが、ナンバーリンクの場合は隣り合ったマス同士をショートカットするようなものも1つの（関西）解になるので、明文で「すべてのマスを通る」という条件をかけてある場合でなければ、このようなパターンが生じた結果「解なし」となることはありません。そして、ショートカットしてできあがるのはもちろん関西解ですので、関西解のない問題にはまったく影響しません。

また、空間が余った場合に、2×2のループが発生することがあります。孤立したループも、隣り合う2マスに同じ数字が入るようなシチュエーションとして、条件を満たしてしまうのです。とはいえ、空間が余っている以上、ループを削ったものも関西解として成立するので、マスの余らない問題にはこれまた影響しない話です。とりあえず、無視して進むことにします。

ルールをSATに変換

ルールを変形したところで、論理式として起こして行きましょう。

準備する変数

変数としては、各マスで、存在しうる数字すべてについて「入るか入らないか」という変数を準備します。なお、すでに数字の入っているマスなど、決め打ちになってしまう変数も発生しますが、この時点で除去しなくてもSATソルバーは充分速く処理してくれるので、処理しやすさを優先して放置します。また、問題によっては補助的な変数が必要となることもありますが、ナンバーリンクの場合は使わなくても処理できました。

最初から数字の入っているマスの場合

最初から数字の入っているマスの場合、条件は次の2つです。

その数字が入る
隣接4マスの中で、ちょうど1マスが同じ数字になる

まず1つ目ですが、あるマスに最初から「2」が入ることになったとしましょう。すると、当然「このマスに2が入る」という変数はtrueですし、残りの「このマスに1が入る」「このマスに3が入る」などはfalseになります。

2つ目の条件については、上のパターンそのままです。「ちょうど1つ」という条件を「1つ以上」と「1つ以下」に分解して、「1つ以上」の方は全部のORを取れば終わりです。「1つ以下」のほうは、2つずつ取って行ってNOTしたものをORして「2ついっぺんにtrueになることはない」として、それを全部ANDすれば条件を満たせます。

たとえば、あるマスに2が入っている時に、上・下・左・右に2が入るという条件変数をそれぞれ $U$、$D$、$L$、$R$ とすると、ちょうど１マスだけ入る条件は、

(U\vee D\vee L\vee R) \wedge (\neg U \vee \neg D) \wedge (\neg U \vee \neg L) \wedge (\neg U \vee \neg R) \wedge (\neg D \vee \neg L) \wedge (\neg D \vee \neg R) \wedge (\neg L \vee \neg R)

のようになります。

数字の入っていないマス

数字の入っていないマスの場合、条件は次の2つになります。

隣り合う最大4マスのうち、（4マスの中で）同じ数字が入るのは2マス以下
隣り合う最大4マスのうち、そのマスと同じ数字が入るのはちょうど2マス

このうち1については少し説明しておきます。まず、仮にあるマス $A$ と隣り合うマスのうち3マスが同じ数字になったとします。もしこの $A$ 自身が3マスと同じ数字になったとすると、それは定式化の際に除外していいとしたパターンです。逆に、$A$ へ別な数字が入るとすると、それは最大1マスとしか同じ数字とつながれないので、$A$ が端っこでないとすればありえません。残るは $A$ が空きマスとなるパターンですが、これにしても空きマスにせず、このマスをショートカットして解を作れるので、（関西解を全パターン求めるという気にでもならなければ）無視できます。

そして、1については、3つ取ってNOTしたものORして、それを全パターンANDするというパターンでできます（もちろん、もともと2マスにしか隣接していなければ自明ですが）。残るは2です。

まず、「ちょうど2マス」という条件になっていますが、1で「2マス以下」はチェック済みなので、考えるべき条件は「2マス以上」だけです。

ただし、「元のマスと同じ」という条件が付いています。これを論理式の形にすると、「あるマスに特定の数字が入るなら、隣接するマスのうち2マス以上に同じ数字が入る」となります。ただし、「ならば」の形ではCNFにならないので、「あるマスに特定の数が入らない、もしくは隣接するマスのうち2マス以上にその数字が入る」となります。

そして、このまま式を立てて行くと、$\neg A\vee ( (ORでつないだ条件1) \wedge (ORでつないだ条件2)\dots )$ という形になって、そのままではCNFとして成立しません。ここでは分配法則を使って、$(\neg A\vee ORでつないだ条件1) \wedge (\neg A\vee ORでつないだ条件2)\dots $と変形することで、CNFとできます。

その他

2015年11月2日はブール氏の生誕200年ということで、Googleロゴも論理式仕様になっていました。

シリーズ記事の一覧

爆速ナンバーリンクソルバー（1）〜ナンバーリンクと充足可能性問題
爆速ナンバーリンクソルバー（2）〜ナンバーリンクのSAT化

（続く）