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

先ほど、ブラウザで動くナンバーリンクソルバー（http://jkr2255.github.io/js_puzzle_solvers/numberlink.html）を公開しました。それについてまとめようと思ったのですが、1本の記事に書くには長すぎるので、少しずつ分けて書いていこうと考えています。

まずは、問題そのものである「ナンバーリンク」と、それの解法に使った「充足可能性問題」について解説します。

まず、「ナンバーリンク」って？

ナンバーリンクは、数独やクロスワードといった、（もともとは）紙と鉛筆で楽しむ「ペンシルパズル」の一種です。ルールはニコリ社のサイトにもありますが、

• 盤面に入っている同じ数字を結ぶ
• 線は交差・分岐・合流などをせず、1マスに1本だけ通る
• 線は縦横に連続したマスにしか引けず、盤面の外にも出ない

というような感じです。

ふつう、数独に代表されるようにペンシルパズルは「ここにはこれが入らないから別のが入る」というように細かな条件を論理的に積み上げていくケースが多いですが、ナンバーリンクにはそのやり方が通用せず、ニコリにも「理詰めよりひらめきが重要」と書かれています。そういうわけで、コンピューターとの相性は決して良くなく、Windows用のソルバーでも15×15を完全に解ききるのに1時間ほどかかるような状況でした。

関西解

ナンバーリンクの用語として「関西解」というものがあります。「線が全部のマスを通らない別解」のことですが、関西の人からの投稿した問題から発見されたとか、関西の人からの指摘で発見されたとかということが多発したためにそう呼ばれるようになったとのことです。ニコリへの投稿では、作者側へのルールとして「すべてのマスを線が通る」というものがかけられています。

もし関西解を無視するなら、「全部のマスに線が通る」ということになり、理詰めで進む部分も増えます。ソルバーでも、関西解を無視した場合にはずっと速く動くものがありました。とはいえ、関西解がないかのチェックもソルバーに求められる役割なので、それは放棄したくないところです。

「充足可能性問題」とは？

今回、ナンバーリンクを解く方法としては、ナンバーリンクの条件を充足可能性問題に変換して、それを解く、という手法を取りました。

充足可能性問題、あまり聞きなれない人も多いとは思いますが、ざっくり説明すればこんな感じです。

trueかfalseを取る大量の変数と、それをAND、OR、NOTで結んだ1本の論理式があって、この論理式全体をtrueにできるような変数の組が存在するか判定する問題

これだけだと使い道がピンとこないと思いますので、数独に当てはめてみましょう。「このマスが1になる」「このマスが2になる」…といった感じで、9×9×9=729個の論理変数を用意します。そして、これらが数独としての条件を満たす（同じ行や列、ブロックに同じ数字が入らない）ように論理式を並べていって、あとは充足可能性問題のソルバーに解かせれば、数独の解が出てくる、という寸法です。

なお、英語名称のSATisfiability Problemsから、略して「SAT」と呼ばれています（本稿でもこの略称を適宜使います）。

また、SATはNP完全性が初めて証明された問題であり、また多くの問題のNP完全性がSATを経由して証明されているという側面もあって、理論上も重要な問題です。

SATとして解くメリット・デメリット

ナンバーリンクを直接解かず、このようにいったんSATとして解くことには、いくつかのメリット・デメリットがあります。

まず、いちばんのメリットとしては、SATソルバーは世界中の研究者がしのぎを削って最速を競いあうような分野なので、そのプラットフォームに乗せてしまえば、何もしなくてもSATソルバーを入れ替えるだけでどんどん速くなる、ということがあります。もちろん、ナンバーリンク専用にプログラムを書けば、理論上はもっと速いものを作れるはずですが、一般のプログラマーにはとうてい無理な芸当なので、プログラミングの手間を考えればSATソルバーを使った解法がじゅうぶんな最適解だと思います。

逆にデメリットとしては、SATソルバーは条件を満たす場合、値を「1組」返して終わってしまうので、別解がないかのチェックが必要となります。とはいえ、「この解を除外する」という条件1つを付け加えてもう一度SATソルバーを回せば、別解があるかどうか判定できますし、それをしてもなお高速です。

CNF形式

SATソルバーは論理式を処理すると上述しましたが、実はその中でも連言標準形（英語のConjunctive Normal Formを略してCNFともいう）という形の論理式しか受け付けないものがほとんどです。CNFは、以下のいずれかのものをAND（$\wedge$）でつないだ形式です。あるいは、以下の3つの形の式を与えて、それらすべてを満たす、と言い換えても本質的に同じです。

• 1つの変数（$A$）
• 1つの変数の否定（$\neg A$）
• 上の2つの形のものをOR（$\vee$）でつないだもの（$\neg A \vee B \vee C \vee \neg D$）

つまり、$\neg(A\vee B)$や$A \vee (B \wedge C)$といったものは入らない、ということになります。もちろん、これらもうまく変形すればCNFにすることができます。ただし、ナンバーリンクを論理式化するに当たって、CNFの枠内ですべてを書けたので、その変換方法については触れません。

関連リンク

• ruby-minisat とパズルのソルバ

シリーズ記事の一覧

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

（続く）