充足可能性問題 (SAT) について わずかに調べた

1. 全体像

SATとかCNF-SATと呼ばれているタイプの問題がある。解きたい課題を 論理学の連言標準形 に翻訳して 求解するというものだ。身近なところだと数独。

数独を解きたい！
  → 数独のルールや初期盤面を論理式に翻訳
  → 論理式を CNF に変形
  → 汎用SATソルバに解かせる
  → 解を数独の解として読み解く

この描像では ポイントは以下の３つといえる（本稿では 翻訳・変形・求解と記載）:

• [翻訳] 現実の課題を 論理式にどう落とし込むか？
• [変形] どうやって簡潔なCNFを作るか？
• [求解] どうやって高速なSATソルバを作るか？

「翻訳」の例。数独では 81マスそれぞれに1..9がそれぞれ入るか？に対応する命題変数を 729個用意し、81個の変数がTrue で648個の変数がFalse となるような解を求めることに帰着できる。

「変形」の例。解きたい課題がCNFでない場合には、変形する必要がある。ドモルガンの法則を使えばCNFに同値変形できることは知られているが、指数オーダーの操作が必要になるので工夫が必要になる。なお、数独の例ではこれは不要 キーワード: Tseitin変換, 充足的同値性

「求解」の例。論理式の充足性は、「登場する変数の個数 n に対して $2^n$ 通りの付値を調べればよく、それ以外に本質的に効率的な方法がない」のが論理学の帰結。だが CNFが特定の形をしていれば 効率よくやる方法がある。またそれを実装に落とし込んだ有名なプログラムもある。キーワード: DPLLアルゴリズム, Minisat

2. 使ってみる

2-1. ファイルフォーマット

SATは毎年の国際的なコンテストなどもあり 標準化が進んでいる。特にCNF をテキストファイルで表現する方法は共通化されている。以下が例:

input.txt

c This is comment
c
p cnf 3 2
1 -3 0
2 3 -1 0

ざっくりとした説明：文頭のc はコメント行を表す。p cnf 3 2において 変数が3つあり節が 2つあることを宣言している（p と cnf はおまじない）。変数 $x_1, x_2, ...$に 1,2,3... を当てる。n の否定は -n を充てる。よって -2 は $\neg x_2$ を表す。0 は 節の境界を表し(必須ではないが)慣例的に行末につける。変数同士のスペースには ⋁ が入っているとみなす。

以上を考えると、上記のファイルは CNF : ($x_1\lor\lnot x_3)\land(x_2\lor x_3\lor\lnot x_1)$ を表現したものだとわかる。

2-2. インストールと実行

SATソルバは色々あるけれど、十分早くて 事実上の参照実装となっているものがある。MiniSatと呼ばれるC++ でオープンソース(MIT)な実装だ。Ubuntu では sudo apt install minisat で一瞬で導入できるし、コンパイルをしても簡単。

インストールすると コマンドラインから $ minisat input.txt output.txt と呼び出せる。先ほどのファイルを使って実行すると以下を得る:

output.txt

SAT
1 2 -3 0

出力の意味は明快で、$x_1, x_2$ をTrue に割り当て $x_3$ に False を割り当てると、与えられたCNF は充足する。手を動かして計算をしてみても、確かにそうなっている。

3. 先に進む

次に何をしよう？

3-1. 翻訳

• 数独を 729個の命題変数の登場する論理式 へと変形するとか、数学の四色問題を対応する論理式へと変形するとか、現実の課題を論理の世界に翻訳することには慣れが必要。
• 計算ドリル的なものはあるのだろうか？競プロ？

3-2. 変形

• ドモルガン則を再帰的に適用することにより 論理式を CNF に変形するというのは、少し複雑な論理式で実践してみると確かに計算量が多いな、と気づく。
• Tseitin変換、充足的同値性を理解して、幾つかの論理式を 充足同値なCNFに変形するのもやってみる。

3-3. 求解

• DPLLアルゴリズムなどの論文・教科書を読み「どんな場合にどんな規則を使うとどれほど楽になるか」についての見解をまとめる。
• MiniSat のコードを読む。コード量自体そんなに多くないらしい。
• たぶんコマンドラインツールではなく、ライブラリとしても使えるのでは？そのあたりのインターフェースを調べる。

3-4. 課題を捉えなおす

• 2-SAT, 3-SAT: 節の長さが2であれば多項式時間で解けて、節の長さが3以上だとそれがむり(指数時間になる)など、SATのある部分においては理論が整備されているらしい
• PB-SAT, CSP-SAT: SATは命題論理なので算術がからむ問題を翻訳するのは骨が折れる。なので PB-SAT とか CSP-SAT など表現力の高い言語で課題を表現し、SATに落とし込むというアプローチがある

参考

• MiniSatのページ: http://minisat.se/Main.html
• 神戸大の人たちの解説記事: https://www.jstage.jst.go.jp/article/jssst/34/1/34_1_67/_pdf