3.5 SAT 問題

複雑な論理式が充足可能かどうかを判定するのは中々骨が折れる。例えば、次の論理式は充足可能だろうか？

論理式が充足可能satisfiableかどうかを判定する一般的な問題を SAT と呼ぶ。SAT を解くアプローチの一つとして、真理値表を構築して \(\textbf{T}\) が現れるかどうかを一行ずつ確認するものが考えられる。しかし、恒真性の判定でもそうだったように、真理値表を使うアプローチは命題変数の個数が増えると所要時間が指数的に増加する。

これより効率的な SAT の解法は存在するだろうか？ 具体的に言えば、\(n\) 個の命題を含む任意の論理式の充足可能性を \(2^{n}\) といった指数時間ではなく \(n^{2}\) や \(n^{14}\) といった多項式時間で判定する素晴らしい手続きは存在するだろうか？ 誰にも分からない。この質問の答えは重大な意味を持つ。

「効率的」な手続きとは、入力の長さを \(s\) としたとき \(s\) の多項式時間で実行できる手続きと一般的に定義されている。この意味で効率的な SAT の解法は、プログラミング、代数、経済、政治をはじめとした様々な分野におけるスケジューリング、ルーティング、資源分配、デジタル回路検証といった重要な問題に対する効率的な解法の存在を直ちに意味する。それなら早く SAT を解くべきだと思うかもしれないが、SAT が解かれると暗号化された文章が簡単に復号できるようになるので、オンライン決済は危険になり、秘密通信は誰にでも解読可能になる。この理由は第 9.12 節で解説される。

もちろん、恒真性の判定を考えたとしても状況は変わらない: 論理式の恒真性は、その否定の充足可能性の否定に等しいからである。この事実は第 3.2 節で触れた論理式の単純化が難しい理由でもある ── 恒真性の判定は「この論理式は \(\textbf{T}\) に単純化されるか？」という単純化の特殊ケースである。

近年、デジタル回路検証といった実用的なアプリケーション向けの SAT ソルバー (SAT-solver) が目覚ましい発展を遂げている。最新の SAT ソルバーを使うと、たとえ数百万個の命題変数が含まれる論理式であったとしても、それを充足させる真理値の割り当てを非常に高い効率で見つけられる場合がある。しかし残念ながら、SAT ソルバーが採用する手法がどのような種類の論理式を上手く扱えるかは予測できない。また、SAT ソルバーは充足不可能性に関しては効率がずっと低い。

SAT を多項式時間で解く方法、あるいはそれが存在しないという証明は知られていない ── 研究者たちは完全に行き詰まっている。「SAT が多項式時間解法を持つか？」という問題は \(\textbf{P}\) 対 \(\textbf{NP}\) 問題 (\(\textbf{P}\) vs. \(\textbf{NP}\) problem) と呼ばれる¹。理論情報科学の分野で長く未解決の問題であり、ミレニアム問題の一つでもある: \(\textbf{P}\) 対 \(\textbf{NP}\) 問題を解くと、Clayクレイ 研究所から百万ドルが授与される。