クック＝レヴィンの定理：最初のNP完全問題としてのSAT

形式的な主張と証明の考え方

形式的には、この定理は決定問題SATがNP困難であり、かつNPに属する、したがってNP完全であると主張する。証明では、任意の非決定性チューリング機械Mと入力xに対し、Mがx上でステップ数が有界な範囲内に受理計算を行う場合に、かつその場合に限って充足可能となるブール式を構成する。通常の符号化では、計算履歴、すなわち構成のタブローを表現し、各時刻における機械の状態、テープ記号、ヘッド位置を表すブール変数を用いる。節によって有効な遷移と受理状態の存在を強制する。この符号化は、元のインスタンスの大きさに対して多項式時間で決定性チューリング機械により生成できるため、任意のNP問題からSATへの多項式時間多対一帰着が得られる。

歴史と発展

この結果は、1970年代初頭に中核となる考え方を独立に発展させたスティーヴン・クックとレオニード・レヴィンにちなんで名付けられた。クックの1971年の論文は西側でこの定理を広く知らしめた一方、レヴィンはソビエト連邦で関連する結果を得た。両者の研究はNP完全性という概念の形式化に直接つながり、その後まもなく多数の自然なNP完全問題を示したリチャード・カープらによる帰着研究を促した。この定理と計算量理論における役割の一般的な導入については、概説資料および標準的な参考文献のような計算理論の文献を参照。

帰結と応用

クック＝レヴィンの定理は、理論面と実用面の両方に帰結をもつ。理論的には、いずれかのNP完全問題に決定性多項式時間アルゴリズムが存在すれば、P = NPとなり、NPに属するすべての問題を効率的に解けることを確立する。実用的には、一見異なる多くの問題がSATへ帰着できるとの認識が、高度に最適化されたSATソルバーや帰着に基づく手法の開発を促した。検証、計画、暗号、組合せ最適化における現実の問題は、しばしばSATのインスタンスとして符号化され、特化したヒューリスティックによって扱われる。応用面の視点については、SATに関する資料でブール充足可能性問題の議論を参照。

関連問題と区別

• SATの変種：3-SATのような特定の制限付き形式はNP完全のままである一方、自明な変種はより容易な場合がある。これは、計算量が問題の制約に敏感であることを示している。
• NP完全という概念：SATはNP完全であることが最初に証明された問題である。クリーク、頂点被覆、部分和など、多くの問題が後に多項式時間帰着によってNP完全と示された。形式的な一覧と例については、NP完全性に関する資料を参照。
• P対NP：この定理はP対NP問題と直接結び付く。NP完全問題に対する効率的な、すなわち多項式時間の決定性アルゴリズムが存在するかどうかは、計算機科学における中心的な未解決問題の一つである。

クック＝レヴィンの定理は、帰着を通じて問題の困難さを比較する明確で構成的な方法を与えるため、計算量理論の礎であり続けている。その影響は純粋理論、アルゴリズム設計、そしてNP完全性の認識が期待や解法戦略を導く多数の応用分野に及ぶ。