充足可能性問題 (SAT) とエンコーディング

論理式を真にする変数割当が存在するかを判定する問題。NP完全問題の原型であり、多くの組合せ問題を SAT へ帰着して SAT solver で解く実用パターンが広い。

Cook-Levin 定理

SAT は NP 完全であることを示した定理。任意の NP 問題は多項式時間で SAT に帰着できる。さらに $\mathrm{SAT}{\le }_{p}3SAT$（節を 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 / binary-decision-diagram / _moc-algorithm