回路充足可能性問題

理論計算機科学では、回路充足可能性問題（ CIRCUIT-SAT、CircuitSAT、CSATなどとも呼ばれる）は、与えられたブール回路の入力の割り当てによって出力が真になるかどうかを判定する決定問題である。 ^{[ 1 ]}言い換えれば、与えられたブール回路への入力を、回路の出力が1になるように一貫して1または0に設定できるかどうかを問う問題である。その場合、回路は充足可能であると呼ばれる。そうでない場合、回路は充足不可能であると呼ばれる。右の図では、左側の回路は両方の入力を1に設定することで充足できるが、右側の回路は充足不可能である。

CircuitSATはブール充足可能性問題（SAT）と密接に関連しており、同様にNP完全であることが証明されています。^{[ 2 ]}これは典型的なNP完全問題であり、Cook-Levinの定理はSATではなくCircuitSATで証明される場合があり、その後CircuitSATを他の充足可能性問題に還元してそれらのNP完全性を証明できます。^{[ 1 ] [ 3 ]}回路の充足可能性には、${\displaystyle m}$任意のバイナリゲートは時間内に決定できる${\displaystyle O(2^{0.4058m})}$[ ^{4 ]​}

回路と適切な入力セットが与えられた場合、各ゲートの出力は定数時間で計算できます。したがって、回路の出力は多項式時間で検証可能です。つまり、回路SATは複雑性クラスNPに属します。NP困難性を示すには、 3SATから回路SATへの還元を構築できます。

元の3SAT式に変数があると仮定します${\displaystyle x_{1},x_{2},\dots ,x_{n}}$、および演算子（AND、OR、NOT）${\displaystyle y_{1},y_{2},\dots ,y_{k}}$. すべての変数に対応する入力と、すべての演算子に対応するゲートを持つ回路を設計します。ゲートは 3SAT 式に従って接続します。たとえば、3SAT 式が次のようになっている場合${\displaystyle (\lnot x_{1}\land x_{2})\lor x_{3},}$回路には 3 つの入力があり、1 つの AND ゲート、1 つの OR ゲート、および 1 つの NOT ゲートがあります。${\displaystyle x_{1}}$ANDゲートに送る前に反転されます。${\displaystyle x_{2},}$ANDゲートの出力はORゲートに送られ、${\displaystyle x_{3}.}$

3SAT式は上記の回路と等価であるため、同じ入力に対して出力は同じになります。したがって、3SAT式に充足可能な割り当てがあれば、対応する回路は1を出力し、その逆もまた同様です。つまり、これは有効な還元であり、回路SATはNP困難です。

これで、回路SATがNP完全であることの証明が完了する。

CircuitSATまたはその派生問題からの還元は、特定の問題のNP困難性を示すために使用でき、デュアルレール還元やバイナリロジック還元に代わる手段を提供する。このような還元で構築する必要のあるガジェットは以下のとおりである。

• 配線模型。この模型は回路内の配線をシミュレートします。
• 分割型デバイス。このデバイスは、すべての出力線が入力線と同じ値を持つことを保証します。
• 回路のゲートをシミュレートする装置。
• まさにターミネーター装置。この装置は、回路全体の出力を強制的に正しい値にするために使用されます。
• 回転装置。この装置を使うことで、必要に応じて配線を正しい方向に誘導できます。
• クロスオーバー装置。この装置を使うと、2本のワイヤーを互いに干渉させることなく交差させることができます。

ツェイティン変換は、回路SATからSATへの単純な還元です。回路が2入力NANDゲート（機能的に完全なブール演算子のセット）だけで構成されている場合、この変換は簡単に説明できます。回路内のすべてのネットに変数を割り当て、次に各NANDゲートに対して、結合標準形節（v ₁ ∨ v ₃ ) ∧（v ₂ ∨ v ₃ ) ∧（¬ v ₁ ∨ ¬ v ₂ ∨ ¬ v ₃）を構築します。ここで、v ₁とv ₂はNANDゲートへの入力であり、v ₃は出力です。これらの節は、3つの変数間の関係を完全に記述します。すべてのゲートからの節を、回路の出力変数が真になるように制約する追加の節と結合すると、還元が完了します。すべての制約を満たす変数の割り当てが存在するのは、元の回路が充足可能である場合に限り、かつその場合に限ります。また、任意の解は、回路の出力が 1 になるような入力を見つけるという元の問題の解です。^{[ 1 ] [ 9 ]}逆、つまり SAT が回路 SAT に還元可能であることは、ブール式を回路として書き直してそれを解くことで自明に導かれます。

• 回路値の問題
• 充足可能性問題