# 充足可能性問題(SAT) ## 定義 充足可能性問題(satisfiability problem, SAT)は、与えられた命題論理式が充足可能(satisfiable、すなわち変数へのある真理値割り当てで式全体を真にできる)かどうかを判定する問題である。真理値表を構成して T の行の有無を調べる素朴な方法は、変数数 n に対して真理値表が 2^n 行になるため指数的な手間がかかる。SAT が多項式時間で解けるかどうかは未解決であり、この問いは「P対NP問題」と呼ばれ、理論計算機科学における最も重要な未解決問題の1つ、かつ Clay 研究所の7つのミレニアム問題の1つに数えられる。効率的な SAT の解法が存在すれば、スケジューリング・経路選択・資源配分・回路検証など多くの重要問題が効率的に解けるようになる一方、暗号化通信の解読も容易になり社会的混乱を招くとされる。妥当性判定は充足可能性判定に帰着できる(命題論理式 P が妥当 iff NOT(P) が充足不能)ため、両者は本質的に同じ計算困難性を持つ。近年の SAT ソルバは実用上は数百万変数規模の式でも高速に充足割り当てを発見できるが、充足不能な式に対しては一般に効果が薄く、どのような式がソルバに向くかを事前に予測するのは難しい。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 3 Logical Formulas]]) ## 横断的知見 （この concept は本 ingest が初出のため、複数ソースの突き合わせによる横断的知見はまだない。他章・他ソースが SAT・P対NP問題・SAT ソルバに触れた際にここへ追記する。） ## 未解決の問い - SAT ソルバが実用上「数百万変数規模でも高速」に動く一方で理論的には NP完全である、という実務と理論のギャップは、どのような式のクラス(構造)によって説明されるか。第3章では述べられていない。 - P対NP問題そのものの現在の研究状況(未解決のまま)について、他の情報理論・暗号関連ソースでの言及と突き合わせられるか。第8章(数論・RSA暗号)の ingest 後に橋渡しできる可能性がある。 ## 関連 - 概念: [[命題論理]] / [[述語論理]] - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 3 Logical Formulas]] ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 3.