5
2

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

爆速ナンバーリンクソルバー(2)〜ナンバーリンクのSAT化

Posted at

(この記事は、連載記事です。ソルバー自体 その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. 次のルールに従って、盤面に1つずつ数字を入れます。
  2. もともと盤面に入っていた数字2つが、同じ数字をタテヨコにたどってつながるようにします。
  3. もともと盤面に入っていた数字については、タテヨコに隣接するマスのうち1つだけに同じ数字が入ります。
  4. 空きマスに入れる数字については、タテヨコに隣接するマスのうちちょうど2つに同じ数字が入ります。

のように変換できます。

変形の代償

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

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

ルールをSATに変換

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

準備する変数

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

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

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

  1. その数字が入る
  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$ とすると、ちょうど1マスだけ入る条件は、

(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つになります。

  1. 隣り合う最大4マスのうち、(4マスの中で)同じ数字が入るのは2マス以下
  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ロゴも論理式仕様になっていました。

シリーズ記事の一覧

(続く)

5
2
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
5
2

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?