充足可能性問題 (SAT) とエンコーディング
論理式を真にする変数割当が存在するかを判定する問題。NP完全問題の原型であり、多くの組合せ問題を SAT へ帰着して SAT solver で解く実用パターンが広い。
Cook-Levin 定理
SAT は NP 完全であることを示した定理。任意の NP 問題は多項式時間で SAT に帰着できる。さらに （節を 3 リテラルに減らす／増やす変換）も成り立つ。
変種
- Circuit-SAT — 論理回路で表現した SAT。これも NP 完全。
DIMACS CNF フォーマット
SAT solver 入力のデファクト標準。p cnf 変数数 節数 ヘッダの後、各節を整数列（負数は否定、行末 0）で書く。
p cnf 2 3
1 2 0
-1 2 0
-1 -2 0
エンコーディングの実践
パズルや制約充足を SAT に落とす。例「犯人は誰だ」では各証言を (!A) == (B || C) のような双条件として書き、CNF 化して solve する。解の否定を制約に追加して再 solve し UNSAT なら一意解、という解の一意性検証テクニックも使える。
関連: np-complexity-classes / boolean-satisfiability-sat / _moc-cs
二分決定図 (BDD / ZDD)
論理関数を表現する DAG 型データ構造。変数を順に分岐させ、同型な部分木を共有することで論理関数を圧縮表現する。
ZDD
Zero-suppressed BDD。集合族（組合せ集合）を表すバリアント。
- 圧縮表現のまま union / intersection / difference といった集合演算を計算できる
- ただし演算が正しく行えるには 簡約化 されている必要がある（冗長な節点が無く、表現が一意であること）
簡約化と並列化
トップダウンに構築した BDD は冗長性が生じやすく、演算ごとに簡約化が必要。
- Knuth09 の簡約化アルゴリズムは
- これをさらに高速化したい → ハードウェアによる高速化、本研究では 並列準簡約化と追駆簡約化 による新しい並列化（先行研究の並列化手法と直交＝因果関係のない別軸の手法）
SAT と同じく論理関数を扱うが、BDD は関数全体を一意な正規形として保持する点が異なる。
関連: boolean-satisfiability-sat / parallel-computing / _moc-cs