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

さて、前回にナンバーリンクのSAT化を行いましたので、あとは実行環境を用意するだけです。ただ、JavaScriptという環境で実用に耐えるだけのSATソルバーがあるのかと思って調べてみたところ…ありました¹。

SATソルバーの世界

まず、何も考えずに原始的な解き方をしてみようとすれば、変数すべてにtrue/falseの取りうるパターンを入れていく、ということになります。これでは変数 $n$ 個の場合に $O(2^n)$ だけの時間がかかってしまいます。そして、SAT問題はNP完全であって、現状では多項式時間で片付くアルゴリズムはありません（もし発見されれば、それがP=NPの証明となります）。

高速に処理しようとすれば、（こういう探索問題全般に共通する手法ですが）可能性のないパターンをどんどん切り捨てる「枝刈り」が必要となってきます。詳しくは別項で触れる予定ですが、90年代後半から枝刈りの手法が進化してきたことでSATソルバーはどんどん高速化し、応用範囲が広がって行きました。

そして、SATが進化する理由のもう1つとして、競技コンテストがある、ということがあります。毎年SATソルバーの性能を競い合う競技会があって、一線の研究者たちがソルバーを持ち込んでしのぎを削っています。しかも、競技に出場するソルバーはオープンソースなので、翌年の参加者は去年のソルバーから進化させて作る、というのがごく当たり前に行われており、それぞれの有利なところを取り入れて年々進化しています²。

MiniSat

そんなSATソルバーの世界の中で有名なソルバーとして、MiniSatがあります。最初に知った時には上記のような事情を知らなかったので、「オープンソースだしMiniだし、どの程度のものを解けるのかな」とあまり期待していなかったのですが、調べてみれば第一線級の優秀なプログラムだと判明してびっくりした次第です。

そして、プログラム自体はC++で書かれており、単体のプログラムとして使う以外に他のプログラムに組み込むこともできます。さらには、他言語へのバインディングも用意されています（もっとも、入出力はテキストで行うので、プログラムとして呼び出すことでも容易に制御できますが）。

Emscripten

とはいえ、クライアントサイドのJavaScriptからC++へのバインディングなど不可能です。そんなわけで、最初からJavaScriptで書かれたソルバーを探していたのですが、なかなか高性能なものが見つかりません。そして、実用的な速度で動くソルバーを見つけたと思ったら、なんと「MiniSatをJavaScriptへコンパイルしたもの」でした（GitHub）。

LLVMといって、コンパイラ型言語にも仮想マシンを仕込んで、プラットフォーム抽象化や高度な最適化を行うシステムがありますが、そのLLVMからJavaScriptへとコンパイルを行えるようにしたものがEmscriptenです。つまりC/C++など、LLVMにできる言語であればおよそ何でもJavaScript化できてしまいます。

ただし、コンパイルされてできあがるJavaScriptはふつうのJavaScriptではなく、LLVMをそのままエミュレーション実行するかのような、低水準なコードとなります。一部だけ取り出して使うことはほぼ不可能で、まるごとJavaScriptから呼び出して使うことになります。

というより、じつは因果関係が逆で、もともとは別な言語で進めていたことだったのですが、調べているうちにJavaScript上で実用性能を叩きだすソルバーを発見したので、使いやすさなどを考えてプロジェクト対象をそっちに切り替えた次第です。 ↩
ある年のこと、去年優秀だった4つのソルバーを適当につないだだけで出してきた人がいたのですが、それが案外に優秀な結果を見せて大騒ぎ、なんてこともあったそうです。 ↩