回路充足可能性問題

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

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

回路と満足できる入力セットが与えられれば、各ゲートの出力を定数時間で計算できます。したがって、回路の出力は多項式時間で検証可能です。したがって、回路 SAT は複雑性クラス NP に属します。NP困難性を示すために、 3SATから回路 SAT への 縮小を構築することができます。

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

3SAT 式は上記で設計された回路と同等であることに注目してください。したがって、同じ入力に対して出力は同じです。したがって、3SAT 式に満足のいく割り当てがある場合、対応する回路は 1 を出力し、その逆も同様です。したがって、これは有効な縮約であり、回路 SAT は NP 困難です。

これにより、Circuit SAT が NP 完全であることの証明が完了します。

ちょうど2つの入力を持つNANDゲートのみを含む平面ブール回路（つまり、基礎となるグラフが平面であるブール回路）が与えられていると仮定します。平面回路SATは、この回路に出力が真となる入力の割り当てがあるかどうかを判断する決定問題です。この問題はNP完全です。さらに、回路内の任意のゲートがNORゲートになるように制約を変更した場合でも、結果として生じる問題はNP完全のままです。^[5]

回路 UNSAT は、与えられたブール回路が、その入力のすべての可能な割り当てに対して false を出力するかどうかを判断する決定問題です。これは回路 SAT 問題の補完問題であり、したがってCo-NP 完全です。

CircuitSAT またはその変種からの縮約は、特定の問題の NP 困難性を示すために使用でき、デュアル レールおよびバイナリ ロジック縮約の代替手段を提供します。このような縮約が構築する必要があるガジェットは次のとおりです。

• ワイヤー ガジェット。このガジェットは回路内のワイヤーをシミュレートします。
• 分割ガジェット。このガジェットは、すべての出力ワイヤが入力ワイヤと同じ値を持つことを保証します。
• 回路のゲートをシミュレートするガジェット。
• True ターミネーター ガジェット。このガジェットは、回路全体の出力を強制的に True にするために使用されます。
• ターン ガジェット。このガジェットを使用すると、必要に応じてワイヤーを正しい方向にリダイレクトできます。
• クロスオーバー ガジェット。このガジェットを使用すると、2 本のワイヤを相互作用せずに交差させることができます。

この問題は、与えられたマインスイーパのボードですべての爆弾を見つけることが可能かどうかを問うものです。これは、Circuit UNSAT問題からの還元によってCoNP完全であることが証明されています。 ^[6]この還元のために構築されたガジェットは、ワイヤ、スプリット、ANDゲート、NOTゲート、およびターミネータです。^[7]これらのガジェットに関して、3つの重要な観察があります。まず、スプリットガジェットは、NOTガジェットおよびターンガジェットとしても使用できます。次に、ANDガジェットとNOTガジェットを構築すれば十分です。なぜなら、これらを一緒にすると、ユニバーサルNANDゲートをシミュレートできるからです。最後に、3つのNANDを交差なしで構成してXORを実装でき、XORはクロスオーバーを構築するのに十分であるため、^[8]これにより、必要なクロスオーバーガジェットが得られます。

Tseytin変換は、 Circuit-SAT からSATへの直接的な縮約です。回路全体が 2 入力NAND ゲート(機能的に完全なブール演算子のセット) で構成されている場合は、変換の記述は簡単です。回路内のすべてのネットに変数を割り当て、各 NAND ゲートに対して、連言正規形節 ( v ₁ ∨ v ₃ ) ∧ ( v ₂ ∨ v ₃ ) ∧ (¬ v ₁ ∨ ¬ v ₂ ∨ ¬ v ₃ ) を構築します。ここで、v ₁とv _{2 は}NAND ゲートへの入力であり、v _{3 は}出力です。これらの節は、3 つの変数の関係を完全に記述します。すべてのゲートの節を、回路の出力変数が true になるように制約する追加の節と結合すると、縮約が完了します。全ての制約を満たす変数の割り当ては、元の回路が充足可能であり、任意の解が回路出力を1にする入力を見つけるという元の問題に対する解である場合にのみ存在します。^{[1] [9]}逆、つまりSATはCircuit-SATに還元可能であることは、ブール式を回路として書き直して解くことで自明になります。

• 回路値問題
• 構造化回路の充足可能性
• 満足度問題