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

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