# The Complexity of Theorem-Proving Procedures > [!abstract] 概要 > 多項式時間限定非決定性チューリング機械によって解かれる任意の認識問題は、与えられた命題論理式が恒真式（tautology）であるかどうかを判定する問題へと「還元」できることが示される。ここで「還元」とは、大まかに言えば、第2の問題を解くための神託（oracle）が利用可能であるならば、第1の問題が決定性多項式時間で解かれ得ることを意味する。この還元可能性の概念から、困難性の多項式次数が定義され、恒真性の判定問題は、与えられた2つのグラフのうち第1のグラフが第2のグラフの部分グラフと同型であるかどうかを判定する問題と同一の多項式次数をもつことが示される。その他の例についても議論される。 ## 論文情報 - **著者**: Stephen A. Cook（[[Stephen A. Cook]]） - **所属**: [[University of Toronto]] - **掲載会議**: *Proceedings of the Third Annual ACM Symposium on Theory of Computing* (STOC '71), pp. 151–158, May 1971. - **DOI**: [10.1145/800157.805047](https://doi.org/10.1145/800157.805047) ## 概要 本論文は、理論計算機科学における最大の問題である「P対NP問題」と「NP完全性（NP-completeness）」の概念を初めて定式化した画期的論文である（クックの定理 / Cook-Levin の定理）。Cook は、自動定理証明手続きの計算限界を解明する動機から、非決定性多項式時間チューリング機械（NDTM）の任意の計算履歴を、CNF（連言標準形）の命題論理式として多項式サイズで符号化できることを証明した。これにより、命題論理式の充足可能性問題（SAT）および恒真性判定問題（Tautology）が、すべての NP 問題の中で最も困難な問題（NP完全問題）であることを世界で初めて論証した。 ## 問題設定 命題論理や述語論理の自動定理証明手続きにおいて、多くのアルゴリズムが入力論理式の長さに対して指数関数的な探索時間を要していた。Cook は、これらの問題に対して多項式時間で動作する決定性アルゴリズムが存在するか否かを問うため、計算モデルとして多項式時間限定の決定性・非決定性チューリング機械を定式化し、問題間の相対的計算困難性を測る「神託機械（query machine）による多項式時間還元」を定義した。 ## 提案手法と主要定理（クックの定理） ### 1. 神託機械と多項式困難度 言語 $S$ のメンバーシップを問う神託を備えた多項式時間限定チューリング機械によって言語 $T$ が認識できるとき、$T$ は $S$ に多項式時間還元可能（$T \le_P S$）であると定義した。 ### 2. 定理 1（クックの定理：Cook's Theorem） > 任意の非決定性多項式時間限定チューリング機械によって認識される言語 $L$ は、命題論理式の充足可能性判定問題（SAT）、あるいは同値として連言標準形（DNF/CNF）の恒真性判定問題へと多項式時間で還元できる。 **証明の要点**: 入力 $w$ に対する非決定性計算の各ステップ $t$（$0 \le t \le p(|w|)$）、テープの各セル $i$、各状態 $q$、各テープ記号 $s$ に対して命題変数を割り当てる： - $P_{s,t,i}$: 時刻 $t$ にセル $i$ の記号が $s$ である。 - $Q_{q,t}$: 時刻 $t$ に機械の状態が $q$ である。 - $S_{k,t}$: 時刻 $t$ にヘッド位置がセル $k$ である。 機械の遷移規則、テープ記号の一意性、ヘッドの局所的移動、初期状態、受理状態到達の条件を、入力長に対する多項式サイズの命題論理式として構成する。この論理式が充足可能であることと、機械が $w$ を受理する有効な計算経路が存在することが同値となる。 ### 3. 部分グラフ同型問題への応用 Cook はさらに、この還元手法を用いて、部分グラフ同型性判定問題（Subgraph Isomorphism）などの組合せ問題が、SAT と同一の多項式次数（NP完全性）を持つことを示した。 ## 新規性と理論的意義 1. **P対NP問題の提起**: 決定性多項式時間（$P$）と非決定性多項式時間（$NP$）の分離可能性を現代的計算量理論の中心的未解決問題として位置づけた。 2. **NP完全性の発見**: 個別のアルゴリズムの高速化ではなく、計算モデルそのものの模倣（シミュレーション）を通じて、あらゆる NP 問題を吸収する「普遍的困難問題」が存在することを証明した。 3. **計算複雑性理論の創始**: 本論文と、これを発展させた Karp（1972）の研究により、現代の計算量理論が独立した学問分野として確立された。 ## 考察 Cook の着想の偉大さは、チューリング機械という計算の物理的・機械的プロセスそのものを、命題論理のブール制約として表現した点にある。この証明技法は以後の計算量理論におけるあらゆる完全性証明（PSPACE完全性、EXPTIME完全性など）の基本パラダイムとなった。 ## 出典 - Stephen A. Cook, "The Complexity of Theorem-Proving Procedures", *Proceedings of the Third Annual ACM Symposium on Theory of Computing*, pp. 151–158, 1971.