NP 完全性は、NP に属するすべての言語を一つの言語へ多項式時間で変換することができるという性質である。Cook–Levin の定理は、Boolean 論理式の充足可能性問題 SAT がこの性質をもつことを示す。本記事では、SAT と連言標準形を定義し、非決定性 Turing 機械の受理計算を有限な計算表として表す。計算表の各行が正当な次配置であるという条件を局所的な CNF 節へ変換し、受理計算と充足割当の対応を両方向に証明する。
1 Boolean 論理式と SAT
変数記号をとする。式は有限文字列として符号化し、変数の添字と括弧を含む符号長を式の長さとする。
定義 1.1. Boolean 論理式 (Boolean formula) は、変数、定数、否定、論理和、論理積から有限回の構成で得られる式である。式に現れる変数への割当 (truth assignment) は、各変数へまたはを対応させる写像であり、演算
によって式の値を定める。値がとなる割当が存在する式を充足可能 (satisfiable) という。
変数または変数の否定をリテラル (literal) という。リテラルの有限個の論理和を節 (clause) といい、節の有限個の論理積である式を連言標準形 (conjunctive normal form)(CNF)という。
正しく符号化された充足可能な Boolean 論理式全体の言語を
とする。不正な式の符号はに含めない。
CNF の節に含めるリテラル数には上限を置かない。特に、本記事は各節を高々三リテラルに制限する 3SAT を扱わない。
命題 1.2.
である。
証明. 入力が正しい Boolean 論理式の符号でなければ拒否する。正しい式なら、に現れる相異なる変数を出現順に列挙する。証明書を各変数の値を表すビット列とし、列挙した変数数と同じ長さであることを確認する。
検証器は構文木の葉から根へ値を計算する。各変数葉には証明書の対応するビットを置き、各否定・論理和・論理積の頂点では子の値から一回の Boolean 演算で値を得る。変数名を表へ登録して参照する処理を単純な逐次探索で実装しても、式の符号長をとすれば時間で終わる。証明書長は式に現れる変数数以下であり、高々である。
が充足可能なら、その充足割当を証明書にすれば検証器は受理する。検証器が受理したなら、証明書が定める割当の下で構文木の根の値がであるため、は充足可能である。§E15.11 定理 3.1によりである。▨
2 NP 困難性と NP 完全性
定義 2.1. 言語がNP 困難 (NP-hard) であるとは、任意の言語について
が成り立つことをいう。が NP 困難かつであるとき、をNP 完全 (NP-complete) という。
NP 困難性だけでは、対象言語自身が NP に属することを要求しない。NP 完全性では、NP への所属と NP の全言語からの帰着を別々に確認する。
命題 2.2.が NP 完全でならば、
である。
証明.§E15.11 命題 1.4によりである。任意のをとる。の NP 困難性からであり、と§E15.11 命題 4.2からである。したがってであり、二つのクラスは等しい。▨
3 有界計算表
Cook–Levin の帰着では、帰着元の言語ごとに非決定性機械を一つ固定する。入力だけが帰着関数の入力であり、の状態集合、テープアルファベット、遷移規則は式サイズに対する定数として扱われる。
を一方向無限の単テープ非決定性 Turing 機械とする。§E15.11 命題 1.3により、NP の定義で用いた読取り専用入力テープと作業テープのモデルから、この標準単テープモデルへ変更しても多項式時間性と受理分枝の存在は保たれる。
長さの入力上の全分枝が段以内に停止するとする。
と置く。固定多項式の値を二進筆算で求めてと比較することにより、はから多項式時間で計算することができる。また、
であるため、はの多項式で上から抑えられる。受理または拒否で早く停止した配置には、記号、ヘッド位置、状態を変えない仮想的な停止後遷移を加える。この規約は受理分枝の有無を変えず、すべての分枝をちょうど段の配置列へ延長する。
テープアルファベットを、状態集合をとし、
をセル記号集合とする。はヘッドがないセルの内容を表し、は状態がでヘッドがそのセルを走査し、セル内容がであることを表す。
時刻と位置がを満たす格子を考える。初期ヘッドは位置にあり、一段で高々一マス動くため、時刻までの実際の計算が位置より右へ到達することはない。
定義 3.1 (計算表変数). 各とに対して Boolean 変数
を置く。は、時刻、位置のセル記号がであることを表す。
さらに、の有限な遷移規則集合をとし、各とに対して変数
を置く。は、時刻からへの遷移で規則を選ぶことを表す。停止後の仮想的な自己遷移もに含める。これらの Boolean 変数を総称して 計算表変数 (computation-tableau variable) という。
遷移選択変数を時刻ごとに一つ置くことにより、非決定的な二つの規則を隣接セルが別々に選ぶ誤った計算表を排除する。
4 CNF 制約の構成
有限集合の変数のうちちょうど一つを真にする条件は、CNF
で表すことができる。この形式を以下で繰り返し用いる。
4.1 セルとヘッドの一意性
各について、にわたるのうちちょうど一つが真であるという節を加える。また、各時刻について
のうちちょうど一つが真であるという節を加える。後者は、各行にヘッドと状態の印がちょうど一つ存在することを保証する。
4.2 初期配置
入力に対し、時刻の各セルを単位節で固定する。なら位置を、位置をそれぞれ、位置を空白記号とする。なら位置をとし、残りを空白にする。
4.3 遷移規則の一意性と適用可能性
各について、にわたるのうちちょうど一つが真であるという節を加える。規則の左辺が状態と走査記号でない場合には、各位置について
を加える。各行にはヘッド印が一つだけ存在するため、真に選ばれた規則はその配置へ適用することができる規則に限られる。
4.4 局所更新
規則を固定する。位置の次のセル記号は、時刻の位置の三つのセル記号とだけから一意に定まる。実際、ヘッドが三セルの外にあれば中央セルは変化しない。ヘッドが中央にあれば、書込み記号と移動方向に従って中央の印を消すか残す。ヘッドが左隣から右へ、または右隣から左へ移る場合には、中央セルへ新状態の印を付ける。位置で左移動を命じた場合には、ヘッドは位置にとどまる。
この局所更新関数を
と書く。規則が三セル内のヘッド印へ適用することができない組や、複数のヘッド印を含む組には、の値を任意に定めて全域関数にする。実際の行ではヘッド印と規則の適用可能性を別の節が保証するため、適用不能な組に割り当てた任意の値は充足可能性に影響しない。
左端の外側にはセル記号集合に属さない固定境界記号を置く。左端専用の局所更新関数
を、現在の位置のセル記号から位置の次のセル記号を返す関数として定める。この関数では、位置で左移動を命じられたヘッドを位置にとどめる。適用することができない組には値を任意に定めて全域関数にする。ではヘッド位置が高々であるため、位置はまだ訪問されていない。そこで、位置の右隣には固定空白記号を置いてを用いる。
各、、、および三つのセル記号に対して、含意
を CNF の一つの節
として加える。左端では、各に対して
を加える。右端では、各に対して
を加える。各行のセル記号が一意であるため、実際の三セルの値に対応する節だけが次行の値を強制する。
4.5 受理条件
時刻に受理状態の印が存在するという一つの節
を加える。停止後の自己遷移によって、時刻で受理状態にあることは、時刻以前に受理したことと同値である。
以上のすべての節の論理積を
とする。
5 計算表と充足割当の同値性
補題 5.1. 時刻との二行がセル・ヘッドの一意性を満たし、時刻で選ばれた規則が唯一のヘッド印へ適用可能であるとする。この二行がすべての局所更新節を満たすことと、第二行が規則による第一行の正しい次配置であることは同値である。
証明. 第二行が正しい次配置なら、内点のセル記号は、左端のセル記号は、右端のセル記号はである。したがって、前件が真になる局所更新節の後件も真であり、他の局所更新節は前件の少なくとも一つのリテラルが偽である。よってすべての節が満たされる。
逆に、すべての局所更新節が満たされるとする。内点では、一意性によって第一行の位置の実際のセル記号が一つずつ定まる。選択規則もに一意に定まるため、実際の三セル記号と選択規則を前件とする節ではすべての否定リテラルが偽になり、
でなければならない。同じ議論を左端では実際の二セルとに、右端では実際の二セルとに適用する。第二行の各位置におけるセル記号も一意であるため、第二行の唯一のセル記号は対応する局所更新関数が指定した記号に等しい。対応する等式がすべての位置で成り立つので、第二行は規則による正しい次配置である。▨
定理 5.2. 任意の入力について、
証明.がを受理するとする。受理分枝を一つ選び、停止後の自己遷移によって長さまで延長する。各時刻と位置について、その計算表に実際に現れるセル記号に対応するだけを真にする。各時刻で実際に選ばれた遷移規則に対応するだけを真にする。
各セルには一つの記号があり、各配置には一つのヘッドがあるため、一意性制約を満たす。時刻は初期配置制約を満たし、選んだ規則は実際に適用した規則なので適用可能性制約を満たす。連続する二行は正しい一段遷移であるため、補題 5.1により局所更新制約を満たす。分枝は時刻までに受理し、その後は受理配置にとどまるので受理節も満たす。したがっては充足可能である。
逆に、を満たす割当が存在するとする。セル一意性により、各にはセル記号が一つ定まり、ヘッド一意性により各行は状態とヘッド位置を一つもつ配置を表す。初期配置節により第行はの初期配置である。
各では遷移選択制約により規則が一つ定まる。適用可能性節によりは第行の状態と走査記号へ適用することができる。補題 5.1により、第行はによる第行の正しい次配置である。に関する帰納法によって、全行が初期配置から始まる一つの実在する計算分枝をなす。受理節により最終行の状態はであるため、この分枝はを受理する。▨
6 式サイズと帰着の計算時間
補題 6.1.を固定すると、の変数数、節数、符号長、およびを出力する時間は、の多項式である。
証明.とは固定機械だけに依存する定数である。セル変数は
個であり、遷移選択変数は個である。
セル記号の一意性には各セル当たり定数個の節しか要らないため、節数はである。ヘッドの存在には各行一つ、ヘッドの一意性には各行で個の二リテラル節を用いるため、全体で個である。遷移選択、初期配置、適用可能性、および局所更新の節数は、各時刻・位置と固定有限集合を走査して作るので個である。受理条件は一つの長い節であり、リテラル数はである。
したがって節とリテラルの総数はである。添字を二進表記する変数名にはビットを要するため、式全体の符号長は
である。
帰着機械は入力長から固定多項式を計算し、上で列挙した順に変数名と節を書き出す。各節の生成には添字に関する多項式時間しか要らず、出力長自体もの多項式である。はの多項式なので、出力時間と出力長はいずれもの多項式である。▨
7 Cook–Levin の定理
定理 7.1 (Cook–Levin の定理). 充足可能性問題は NP 完全である。
証明.命題 1.2により、である。
任意の言語をとる。§E15.11 定義 1.2により、を受理する多項式時間非決定性 Turing 機械が存在する。を固定し、入力に対して
と定める。補題 6.1により、は多項式時間で計算される。定理 5.2により、
したがってである。は任意であったため、は NP 困難である。NP への所属と合わせて、は NP 完全である。▨
例 7.2 (小さな CNF の充足割当). CNF
を考える。割当では二つの節がともに真になり、式全体が真になる。では第二節が偽になる。
計算表の符号化でも、各節は同じように許されない局所選択を排除する。一意性節は二つのセル記号を同時に選ぶ割当を排除し、局所更新節は前の三セルと選択規則が定まったときに誤った次セルを選ぶ割当を排除する。個々の節は局所的であるが、すべての節の論理積が計算表全体の整合性を保証する。
9 演習
問題 9.1.
解答 (演習の要点).
- 証明書は、式に現れる相異なる変数それぞれに対する一ビットである。各変数は式の符号の中で少なくとも一文字を占めるので、相異なる変数の個数は符号長以下である。したがって証明書長も以下であり、入力長の多項式である。二進添字を用いる符号では一つの変数が複数文字を占めるため、変数の個数はさらに小さくなる。
- 一つの配置から次の配置への遷移は、ただ一つの規則によって定まる。セルごとに独立に規則を選ぶことを許すと、ある位置は規則の局所更新に従い、別の位置は規則の局所更新に従う行が現れる。たとえば、がヘッドの右移動を、が左移動を命じる場合、次の行のヘッド印の位置はとのどちらの配置とも一致しない。局所条件はすべて満たされていても、その行はのどの一段遷移の結果でもない。
- 二箇所で用いる。第一に、第一行の位置の記号がそれぞれ一つに定まることを用いて、否定リテラルがすべて偽になる局所更新節をちょうど一つ特定する箇所である。一意性がなければ、複数の三つ組に対応する節が同時に前件を満たし、互いに異なる後件を強制することがあり得る。第二に、第二行の位置の記号が一つに定まることを用いて、強制されたからその位置の記号がに等しいと結論する箇所である。
- 各行のヘッド印の候補は、位置との組であり、が定数なので個である。そのうち二つを選ぶ組は個であり、行は個あるから、全体で個の二変数節を要する。はの多項式であるからもの多項式であり、各節の書き出しに要する時間も添字に関する多項式である。したがって帰着関数は多項式時間で計算される。
- 停止後の自己遷移は記号、ヘッド位置、状態のいずれも変えない。したがって、時刻で受理状態に到達した分枝は時刻まで受理状態にとどまり、延長後の分枝は時刻で受理状態にある。逆に、延長後の分枝が時刻で受理状態にあるとする。自己遷移は状態を変えないので、受理状態に初めて入る時刻が存在し、時刻までの配置列は自己遷移を含まない。よって、それは元の機械の受理分枝である。ゆえに、延長の前後で受理分枝の有無は変わらない。
▨