命題論理の充足可能性判定問題(SAT:Boolean SAtisfiability)の概要と実装

イントロダクション

AIの目的は、人間が行っているような知的なタスクを実現することであり、そのためには、与えられた情報から新たな情報を導き出すことが必要とされる。このような情報の導出には、推論が不可欠となる。この推論という機能には大きく分けて2つの領域が存在する。

一つは、与えられた前提とルールに基づいて、新たな情報を導き出す推論で、これは”ルールベースと知識ベースとエキスパートシステムと関係データ“に述べられているような、論理や知識を使った推論エンジンを用いるもので、推論エンジンは、与えられた前提とルールに基づいて、保持している情報の中から新たな情報を探索して導き出すものとなる。このような推論エンジンには、エキスパートシステムや診断システムなどの応用分野で活用されているものがある。

またそのような推論においては、様々な推論の手法(手順)も存在する。それらには、”科学的思考(2)仮説検証の為の推論パターン“で述べているように演繹法、帰納法、投射法、類比法、アブダクション法等様々なパターンがある。

もう一つの推論は、”機械学習技術“で述べているような機械学習で、大量のデータからパターンを学習することで、新たなデータに対して予測を行うもので、この機械学習による予測機能も、推論と呼ばれるものとなる。

さらに”論理やルールと確率/機械学習の融合“で述べられているように、これらの2つを組み合わせた推論技術も存在する。

今回はこれらの推論技術の中から、与えられた前提とルールに基づいて、新たな情報を導き出す、論理基づく推論に利用されるSAT(Boolean SAtisfiability;充足可能性判定問題)に関連する技術について述べる。

SAT(Boolean SAtisfiability;充足可能性判定問題)について

命題論理の充足可能性判定問題 (SAT: Boolean Satisfiability) とは、与えられた命題論理式が真となる変数の割り当てが存在するかどうかを判定する問題となる。例えば、「A かつ (B または C) かつ (D または E または F) が真であるような A, B, C, D, E, F の割り当てが存在するかどうか」という問題があった場合、これを命題論理式に変換し、その式が充足可能かどうかを判定するものとなる。

このような問題設定は、例えば、回路設計やプログラム解析、人工知能分野の問題、暗号理論など、多くの応用分野で重要な役割を果たしている。理論的な側面で見ると、SAT問題が解けるアルゴリズムは、「NP完全問題」であることが知られており、現在のコンピュータでは大規模な問題に対しては効率的な解法が見つかっていない。そのため、高速化や、ヒューリスティック探索アルゴリズムの開発などアルゴリズム効率化の為の研究が現在も行われている分野の技術となる。

ここで「NP完全問題」とは多くの場合「NP問題」に属する問題となり、ここでNPとはNon-deterministic Polynomial timeの略で、与えられた解候補が正しいかどうかを多項式時間で検証できる問題のクラスを指す。これは「解が与えられれば，それが問題の制約を満たしているのは容易に確かめられるが，その解を見つけ出すのが困難」な問題ということであり、もう少し砕けた表現だと「検算は簡単だが解を求めるのは難しい問題である」というものとなる。

このNP問題に関して「２１世紀の７大数学予想」として有名なものとして、未証明の数学的証明である「Ｐ≠ＮＰ予想」がある。これはP(polynomial-time:多項式時間計算可能な問題の集合)とNP(nondeterministic polynomial-time:解検証が多項式時間計算可能な問題の集合)は等しくないという予測で、もし，P=NPなら今まで解けなかったNPの問題が全て多項式時間で解けるようになってしまうので，そんな都合の良いことはないだろうという予想となる。ちなみに，P=NPだと素因数分解の難しさを利用した現代の主要な暗号は破られてしまう。

このＰ≠ＮＰ予想に関する参考図書としては、入門的なものとして「「Ｐ≠ＮＰ」問題 現代数学の超難問」や「今度こそわかるＰ≠ＮＰ予想」等がある。

SATソルバー

SATソルバーの話に戻ると、SATソルバーは前述のように、命題論理式を入力として受け取り、その充足可能性を判定するプログラムであり、命題論理式が充足可能かどうかを効率的に判定するために開発されたアルゴリズムに基づいて動作するものとなる。

SATソルバーは、半導体チップの自動設計やソフトウェア工学などの分野でよく使われているツールの一つとなる。例えば”コンピューターを構成する計算要素と半導体チップについて“で述べたように、半導体チップはオン/オフのスイッチングを行うトランジスタを用いて、所望の結果が得られるように論理素子の組み合わせたものによって実現されている。SATソルバーは、このようなハードウェアの検証に利用され、回路が期待通りに動作するかどうかを確認するため、論理回路の充足可能性を判定することができるものとなる。

またソフトウェアの検証という側面でもSATソルバーは活用されている。具体的にはプログラムの仕様をBoolean論理式や制約充足問題(CSP)の形式で表現し、SATソルバーを用いることでプログラムがその仕様を満たしているのかどうかをチェックしたり、コンパイラが生成するコードが特定の入力に対して正しい出力を生成するかどうか、あるいはコードの普遍条件が保持されているかどうかをチェックしたり、SATを使ったソフトウェア検証は非常に正確であることが知られている。

このようなものの一つとしてalloyがある。SATをベースとしたプログラムの仕様チェックツールであるalloyは、アプリケーションの機能、振る舞い、およびインタフェースを表現したモデルを論理的仕様として記述し、自動的で検証を行うものとなる。

抽象によるソフトウェア設計 ―Alloyではじめる形式手法

SATソルバーのアルゴリズムは、主に二つのカテゴリーに分けられる。一つは完全探索アルゴリズムであり、もう一つは非完全探索アルゴリズムとなる。

• 完全探索アルゴリズム: 完全探索アルゴリズムは、命題論理式の全ての割り当てについて探索を行い、充足可能性を確認する。主なアルゴリズムとしては、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムがある。DPLLアルゴリズムは、再帰的に探索空間を探索し、単一リテラル規則、単一節規則、分割規則を使用して、充足可能性を確認する。
• 非完全探索アルゴリズム: 非完全探索アルゴリズムは、完全探索アルゴリズムよりも効率的なアルゴリズムとなる。主なアルゴリズムとしては、WalkSAT、GSAT、CDCL (Conflict-Driven Clause Learning) アルゴリズムがある。これらのアルゴリズムは、ランダム化や学習の手法を使用して、充足可能性を見つける為、DPLLアルゴリズムより効率的なアルゴリズムとなる。CDCLアルゴリズムは、DPLLアルゴリズムの発展形で、より高速で効率的なSATソルバーとして広く使用されている。
• その他アルゴリズム: SATソルバーは、並列計算などの最新のテクノロジーも使用して、高速化される。最近では、GPUを使用したSATソルバーや、量子コンピュータを使用したSATソルバーの研究も進んでいる。

そのようなアルゴリズムを用いたSATソルバーは数多く存在しSAT Competitionにて評価が行われている。”SAT ソルバーの最新動向と利用技術“では少し古い情報となるが、それらSATソルバーに関する情報がまとめられている。ここでは一部代表的なSATソルバーについて述べる。

• MiniSat: 現在最もよく使われているSATソルバーの一つで、高速で高い効率を持つ。
• Glucose: MiniSatから派生したSATソルバーで、MiniSatよりも高速であるとされている。
• Lingeling: SATコンテストにおいて高い性能を発揮しているSATソルバーで、大規模な問題にも対応可能なものとなる。
• CaDiCaL: 並列処理に対応しているSATソルバーで、高速な演算性能を持つ。
• PicoSAT: 小型でシンプルなSATソルバーで、様々なプラットフォームに対応している。

その他にも、SATソルバーにはzChaff、WalkSAT、GRASP、CryptoMiniSat、MapleSAT、Scavelなどがある。

SATソルバーを人工知能技術と組み合わせた応用事例

SATソルバーはソフトウェアやハードウェアの自動検証以外にも、機械学習や人工知能技術を組み合わせることで、複雑な問題に対する高速かつ正確な解法を実現することができる。以下に代表的な応用事例について述べる。

• コンピュータセキュリティの強化

SATソルバーは、セキュリティ分野において、パスワードの解読や暗号化の破解などに利用され、機械学習技術を組み合わせることで、既存の手法では解決が困難な高度な攻撃に対応することができる。具体的にはセキュリティポリシーがどのように動作するかを確認するため、SATソルバーを用いて論理式の充足可能性を判定したり、SATソルバーを用いて暗号化の解読を試みることができる。

• 機械学習分野への適用

SATソルバーは、人工知能分野においても利用することができる。例えば、機械学習においては、モデルをトレーニングするためのパラメータの最適化のケースにおいて、SATソルバーを用いることで、効率的にパラメータの最適化問題を行うことができる。

• 組み合わせ最適化問題の解決

SATソルバーは、組み合わせ最適化問題に対しても利用される。それらは具体的には、物流の最適化やスケジューリング問題などが挙げられる。さらに機械学習技術を組み合わせることで、より高速で正確な解法を実現することもできる。

• 自然言語処理の高速化

SATソルバーは、自然言語処理の高速化にも利用される。これは例えば、文書検索や文書分類などが挙げられる。機械学習技術を組み合わせることで、高速で正確な検索や分類を実現することができる。

• チェスなどのボードゲームのAI開発

SATソルバーは、ボードゲームのAI開発にも利用される。例えば、チェスや囲碁などのゲームの盤面の状態を命題論理式に変換し、SATソルバーで最適な手を探索することができる。さらにこれらに強化学習などの機械学習技術を組み合わせることで、より高度なプレイが実現することが期待される。

SATの参考図書

SATの参考図書としては”論文作成の世界標準ツールであるTex/Latexとウェブ数式表示ツールのMathjax“でも述べたドナルド・E・クヌースによるThe Art of Computer Programmingのシリーズである「The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability」が著名なものとなる。

この図書の序文は以下のようになる。「この冊子は、『コンピュータ・プログラミングの技術』第4巻のFascicle 6です： 組合せアルゴリズム」です。第1巻の巻頭言で説明したように、私がこのような予備的な形で資料を配布しているのは、第4巻の完成には長い年月がかかるとわかっているからです。 この長い文章は、組合せアルゴリズムに関する長い長い章の7.2.2.2節を含んでいます。第7章は、最終的に少なくとも4巻（すなわち4A、4B、4C、4D巻）を埋めることになる。第4巻Aでは、グラフ理論の短い復習と “0と1″（第7.1節）の長い議論から始まり、その巻は第7.2節 “あらゆる可能性の生成 “の最初の部分である第7.2.1節の「基本組合せパターンの生成」で締めくくられています。第4巻Bでは、7.2.2節でバックトラック全般について話を再開し、7.2.2.1節でバックトラック中にデータ構造を更新するための「ダンシングリンク」という手法の一群を説明する予定である。そして、7.2.2.1節では、バックトラック中にデータ構造を更新するための「ダンシングリンク」と呼ばれる手法の一群について説明します。これが本節の舞台となり、これらのアイデアをブール充足性、別名「SAT」の重要問題に適用します。7.2.2.2節は、「SAT」の中で最も長い節となります。SATの問題は明らかにキラーアプリとなります、 なぜなら、それが他の多くの問題を解決する鍵になるからです。このセクションを別のサブセクションに分割するきれいな方法はありませんでした。(そしてとにかくTAOCPのフォーマットでは7.2.2.2.1項を設けることはできない)。私は、右側の各ページの上部に小見出しを追加することで、読者のナビゲーション問題を改善しようとしました。さらに、他のセクションと同様に 練習問題は、本文中の対応するトピックの取り上げ方とほぼ同じ順序で掲載されています。多数のクロスリファレンスが用意されています。
満足度が重要なのは、ブール代数が非常に多用途であることが主な理由です。ほとんどすべての問題は、基本的な論理演算の観点から定式化することができる、 であり、その定式化は非常に多くのケースで特に単純である。7.2.2.2節 は、大きく異なる10の典型的な応用例で始まり、次のように締めくくります。これらの問題は、すべてSATの特殊なケースであることがわかります。116と117（この本の中で一番好きなページです）。満足度の話は、ソフトウェア工学の勝利の話である、 美しい数学をふんだんに使っています。エレガントな新しいデータのおかげで 構造などの技術を駆使して、最新のSATソルバーが日常的に扱えるようになりました。7.2.2.2節では、このような奇跡がいかにして起こったかを、7つのSATソルバーの完全な詳細を提示することで説明している。アルゴリズムA、BからアルゴリズムW、L、Cの最先端手法へ。(まあ、少しはヘッジしないといけませんね： 新しい技術は常に発見され続けています、 そのため、SATの技術はどんどん進化し、ストーリーは進行していきます。アルゴリズムW、L、Cは、最良のアルゴリズムと合理的に比較できること 2010年当時は、そのクラスで知られていたものです。もはや最先端ではありません、 しかし、それでも驚くほどの出来栄えです)。
この本は300ページ以上ありますが、もっと多くのことが分かっているので、私は常に「カット、カット、カット」しなければなりませんでした。書いている最中も、まだ未解明の興味深いトピックが次々と出てきて、一生かかっても足りないくらいでした。それでも、私は前に進まなければならないと思いました。そこで、時間が経つにつれて最も重要になると思われる概念のうち、かなりの部分を選んでここで扱ったつもりである。この資料を作成するために、私は300以上のコンピュータ・プログラムを書きました。なぜなら、プログラミングをしてみなければ、物事は理解できないからです。
もちろん、これらのプログラムのほとんどは非常に短いものですが、そのうちのいくつかはかなり充実したもので、他の人にとっても興味深いものでしょう。そこで、その一部を次のウェブページに掲載しました。http://www-cs-faculty.stanford.edu/~knuth/programs.html このページから SATexamples.tgz をダウンロードすることもできます。
第4B巻は、”Mathematical Preliminaries Redux “と題する番号なしのセクションで、確率論の特別なチュートリアルとレビューで始まります。その方程式や練習問題への言及には、「MPR」という略語が使われています。(以下略 “improvement “という単語があります）」

SATの実装例

• 高度なグラフアルゴリズム(強連結成分分解、DAG、2-SAT、LCA)

高度なグラフアルゴリズムで述べた2-SATは、シンプルなSATの活用事例のひとつとなる。ここでは”Priest Hohn’s Busiest Day”問題として、司祭が複数の結婚式に出席するときの可能なスケジュールの自動判定を行なっている。

• Pythonで論理式を簡単に解くSATソルバー/SMTソルバーZ3の基本的な使い方まとめ(外部リンク)

マルチプラットフォーム対応のSATソルバーであるZ3のpythonによる利用の記事。高速化を考えるとCでビルドして使うケースもあるが、使い方に慣れるには、”pip install z3-solver”でインストールして、後は普通のpyhtonとして使えるものがベター。

• PySAT(外部リンク)

PySATは、広く使われている最先端のSATソルバーを多数統合している。提供されるソルバーはすべて、PySATと一緒にインストールされるオリジナルの低レベル実装となる。ソルバーのソースコードはプロジェクトのソースツリーの一部ではなく、PySATをインストールするたびにダウンロードされ、パッチが適用される。(CaDiCaL (rel-1.0.3)、CaDiCaL (rel-1.5.3)、Glucose (3.0)、Glucose (4.1)、Lingeling (bbc-9230380-160707)、MapleLCMDistChronoBT (SAT competition 2018 version)、MapleCM (SAT competition 2018 version)、Maplesat (MapleCOMSPS_LRB)、Mergesat (3.0)、Minicard (1.2)、Minisat (2.2 release)、Minisat (GitHub version))

• Rolling stones(external link)

Rolling Stonesは、Sat4jのSATソルバーへのClojureインターフェースとなる。SATソルバーは、与えられたブール式が満足できるかどうか、つまり、式全体を真にするブール変数の真理値の割り当てが存在するかどうかを決定するために、総当たり検索と巧妙なヒューリスティックの組み合わせを使用する。

[rolling-stones "1.0.3"]

(require '[rolling-stones.core :as sat :refer [! at-least at-most exactly]])

=> (sat/solve [[1] [1 2] [-1 2 -3]])
[1 -2 -3]

=> (sat/solutions [[1] [1 2] [-1 2 -3]])
([1 -2 -3] [1 2 -3] [1 2 3])