3 SAT (CircuitSAT からの帰着)

様々な問題の NP 困難性を証明するのに特に便利な \(\textsc{SAT}\) の特殊ケースがあり、\(\textsc{3CNF-SAT}\) あるいは \(\textsc{3SAT}\) と呼ばれます。

ブール式が連言標準形 (conjunctive normal form, CNF) であるとは、式がいくつかの節 (clause) の連言 (disjunction, \(\textsc{Or}\)) であり、それぞれの節がリテラルの選言からなる (conjunction, \(\textsc{And}\)) ことを言います。ここでリテラルは一つの変数またはその否定です。例えば: \[ \overbrace{(a \lor b \lor c \lor d)}^{\text{節 (clause)}} \land (b \lor \overline{c} \lor \overline{d}) \land (\overline{a} \lor c \lor d) \land (a \lor \overline{b}) \] は CNF 式です。3CNF 式とは 全ての節が三つのリテラルからなる CNF 式のことです。上の式では最初の節にはリテラルが 4 つ、最後の節にはリテラルが 2 つあるので 3SAT ではありません。3CNF 式が与えられたときに、その式が \(\textsc{True}\) に評価されるような変数への真偽値割り当ては存在するでしょうか?

\(\textsc{3SAT}\) を一般的な \(\textsc{SAT}\) からの帰着で示すこともできますが、\(\textsc{CircuitSAT}\) からの帰着を作って "最初から" 示した方が簡単です。

\(\textsc{CircuitSAT}\) から \(\textsc{3SAT}\) への多項式時間帰着
図 12.5
\(\textsc{CircuitSAT}\) から \(\textsc{3SAT}\) への多項式時間帰着

任意のブール回路 \(K\) が与えられたとき、次に示すステージを経ることで \(K\) を同値な 3CNF 式に変換できます。各ステージを説明すると同時にその正しさの証明も行います。

例えば例として出した回路は次の 3CNF 式となります: \[ \begin{aligned} & (y_1 ∨ x_1 ∨ x_4) ∧ (y_1 ∨ x_1 ∨ z_1) ∧ (y_1 ∨ x_1 ∨ z_1) ∧ (y_1 ∨ x_4 ∨ z_2) ∧ {} \\ & (y_1 ∨ x_4 ∨ z_2) ∧ (y_2 ∨ x_4 ∨ z_3) ∧ (y_2 ∨ x_4 ∨ z_3) ∧ (y_2 ∨ x_4 ∨ z_4) ∧ {} \\ & (y_2 ∨ x_4 ∨ z_4)∧ (y_3 ∨ x_3 ∨ y_2) ∧ (y_3 ∨ x_3 ∨ z_5) ∧ (y_3 ∨ x_3 ∨ z_5) ∧ {} \\ & (y_3 ∨ y_2 ∨ z_6) ∧ (y_3 ∨ y_2 ∨ z_6) ∧ (y_4 ∨ y_1 ∨ x_2) ∧ (y_4 ∨ x_2 ∨ z_7) ∧ {} \\ & (y_4 ∨ x_2 ∨ z_7) ∧ (y_4 ∨ y_1 ∨ z_8) ∧ (y_4 ∨ y_1 ∨ z_8) ∧ (y_5 ∨ x_2 ∨ z_9) ∧ {} \\ & (y_5 ∨ x_2 ∨ z_9) ∧ (y_5 ∨ x_2 ∨ z_{10}) ∧ (y_5 ∨ x_2 ∨ z_{10}) ∧ (y_6 ∨ x_5 ∨ z_{11}) ∧ {} \\ & (y_6 ∨ x_5 ∨ z_{11}) ∧ (y_6 ∨ x_5 ∨ z_{12}) ∧ (y_6 ∨ x_5 ∨ z_{12}) ∧ (y_7 ∨ y_3 ∨ y_5) ∧ {} \\ & (y_7 ∨ y_3 ∨ z_{13}) ∧ (y_7 ∨ y_3 ∨ z_{13}) ∧ (y_7 ∨ y_5 ∨ z_{14}) ∧ (y_7 ∨ y_5 ∨ z_{14}) ∧ {} \\ & (y_8 ∨ y_4 ∨ y_7) ∧ (y_8 ∨ y_4 ∨ z_{15}) ∧ (y_8 ∨ y_4 ∨ z_{15}) ∧ (y_8 ∨ y_7 ∨ z_{16}) ∧ {} \\ & (y_8 ∨ y_7 ∨ z_{16}) ∧ (y_9 ∨ y_8 ∨ y_6) ∧ (y_9 ∨ y_8 ∨ z_{17}) ∧ (y_9 ∨ y_6 ∨ z_{18}) ∧ {} \\ & (y_9 ∨ y_6 ∨ z_{18}) ∧ (y_9 ∨ y_8 ∨ z_{17}) ∧ (y_9 ∨ z_{19} ∨ z_{20}) ∧ (y_9 ∨ z_{19} ∨ z_{20}) ∧ {} \\ & (y_9 ∨ z_{19} ∨ z_{20}) ∧ (y_9 ∨ z_{19} ∨ z_{20}) \end{aligned} \]

この式は一見すると元の回路よりもはるかに複雑に見えますが、各ゲートが最大でも五つの節に変換されることから分かるように、実際には定数倍しか大きくありません。回路の大きさに対する式の大きさが (\(n^{374}\) のような) 次数の大きな多項式になったとしても、NP 困難性を示すための帰着としては何ら不都合はありません。

以上の帰着によって、任意のブール回路 \(K\) は多項式時間で 3CNF 式 \(\Phi_{3}\) に変換できます。また \(K\) を充足させる任意の入力は \(\Phi_{3}\) を充足させる入力に変換でき、その逆も行えます。言い換えれば「\(K\) が充足可能 \(\iff\) \(\Phi_{3}\) が充足可能」ということです。よってもし \(\textsc{3SAT}\) が多項式時間で解けるならば \(\textsc{CircuitSAT}\) も多項式時間で解くことができ、P=NP です。以上より、\(\textsc{3SAT}\) が NP 困難であると結論できます。


  1. 各節のリテラルが最大でも三つであるような連言標準形 \(\Phi_{2}\) を使ってブール回路 \(K\) を表すためのこの方法は、1966 年に Grigorii Tseitin (グリゴリイ・セイティン) によって示されています。 1966 年というのは Levin が prebor problems に対する結果を公表する五年前です。同じ論文で Tseitin は、私たちが現在 \(\textsc{CNF-SAT}\) と呼ぶ問題をおそらく世界で初めて定義しています。[return]

広告