回路充足可能性問題

左の回路は充足可能だが、右の回路は充足不可能である。

回路充足可能性問題（かいろじゅうそくかのうせいもんだい、テンプレート:Lang-en-short、CIRCUIT-SAT、CircuitSAT、CSAT とも表記）は、理論計算機科学における決定問題の一つであり、与えられたブール回路の入力に、出力を真にするような値の割当てが存在するか否かを判定する問題である。言い換えれば、与えられたブール回路の入力を1または0のいずれかに一貫して設定して、回路の出力が1になるようにできるかを問う。もしそれが可能であれば、その回路は「充足可能」と呼ばれる。そうでなければ「充足不可能」と呼ばれる。図の左側の回路では両方の入力を1にすることで充足できるが、右側の回路は充足不可能である。

CircuitSAT はブール充足可能性問題 (SAT)と密接に関連しており、SAT と同様にNP完全であることが証明されている。これは典型的な NP完全問題であり、テンプレート:仮リンクは SAT ではなく CircuitSAT に対して証明されることがある。そして CircuitSAT を他の充足可能性問題へと帰着することによって、それらの問題の NP完全性を示すことができる。任意の 2 入力ゲート $m$ 個を含む回路の充足可能性は $O(2^{0.4058m})$ 時間で判定できる。

NP完全性の証明

回路と充足させる入力の組が与えられれば、各ゲートの出力を定数時間で計算できる。よって回路の出力は多項式時間で検証可能であり、Circuit SAT は複雑性クラス NP に属する。NP困難性を示すには、3SAT から Circuit SAT への還元を構成すればよい。

元の 3SAT 論理式が変数 $x_1,x_2,\dots ,x_n$ と演算子（AND, OR, NOT）$y_1,y_2,\dots ,y_k$ をもつと仮定する。各変数に対応する入力と各演算子に対応するゲートをもつ回路を設計する。ゲートは 3SAT 論理式に応じて接続する。例えば 3SAT 論理式が $(\mathrm{\neg }{x}_1\wedge x_2)\vee x_3$ ならば、回路は 3 個の入力、1 個の AND、1 個の OR、1 個の NOT ゲートを持つ。$x_1$ に対応する入力は、$x_2$ とともに AND ゲートに送られる前に反転され、AND ゲートの出力は $x_3$ とともに OR ゲートへ送られる。

3SAT 論理式は上で設計した回路と等価であり、同じ入力に対して同じ出力を与える。したがって、3SAT 論理式に充足させる割当てが存在するならば、対応する回路は 1 を出力し、その逆も成り立つ。以上より、この構成は妥当な還元であり、Circuit SAT は NP困難である。

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

制限された変種と関連問題

平面 Circuit SAT

2 入力の NAND ゲートのみを含む平面ブール回路（すなわち基礎となるグラフが平面的なブール回路）が与えられたとする。平面 Circuit SAT は、この回路が出力を真にするような入力の割当てを持つか否かを判定する問題である。この問題も NP完全である。さらに、制約を変更して回路内の任意のゲートが NOR ゲートであるとしても、得られる問題は依然として NP完全である。

Circuit UNSAT

Circuit UNSAT は、与えられたブール回路が入力のあらゆる割当てに対して偽を出力するか否かを判定する問題である。これは Circuit SAT 問題の補問題であり、したがってテンプレート:仮リンクである。

CircuitSAT からの還元

CircuitSAT やその変種からの還元は、特定の問題の NP困難性を示すために用いることができ、デュアルレール還元や二進論理還元に代わる手段となる。そのような還元を構成する際に必要となるガジェットは次のとおりである。

• 配線ガジェット。回路の配線をシミュレートする。
• 分岐ガジェット。すべての出力配線が入力配線と同じ値を持つことを保証する。
• 回路のゲートをシミュレートするガジェット。
• 真の終端ガジェット。回路全体の出力を真に強制するために用いる。
• 曲げガジェット。必要に応じて配線の向きを変更する。
• 交差ガジェット。2 本の配線が相互作用せずに交差できるようにする。

マインスイーパの推論問題

この問題は、与えられたマインスイーパの盤面ですべての地雷の位置を特定できるかを問うものである。回路 UNSAT 問題からの還元によりテンプレート:仮リンクであることが証明されている。この還元のために構成されるガジェットは、配線、分岐、AND ゲートと NOT ゲート、および終端である。これらのガジェットについては 3 つの重要な観察がある。第一に、分岐ガジェットは NOT ガジェットや曲げガジェットとしても使える。第二に、AND ガジェットと NOT ガジェットを構成すれば十分である。両者を組み合わせれば汎用の NAND ゲートをシミュレートできるからである。最後に、3 つの NAND を交差なしに組み合わせれば XOR を実装でき、XOR があれば交差を構築できる。これにより必要な交差ガジェットが得られる。

ツァイティン変換

テンプレート:Main テンプレート:仮リンクは Circuit-SAT からSAT への直接的な還元である。回路が完全に 2 入力のNAND ゲート（関数完全なブール演算子の集合）で構成されている場合、変換は簡単に記述できる。回路のすべてのテンプレート:仮リンクに変数を割り当て、次に各 NAND ゲートに対して連言標準形の節 (v₁ ∨ v₃) ∧ (v₂ ∨ v₃) ∧ (¬v₁ ∨ ¬v₂ ∨ ¬v₃) を構成する。ここで v₁ と v₂ は NAND ゲートの入力、v₃ は出力である。これらの節は 3 つの変数の関係を完全に記述する。すべてのゲートから得られる節に、回路の出力変数を真に強制する追加の節を連言結合すれば還元が完了する。すべての制約を満たす変数の割当てが存在するのは、元の回路が充足可能であるのと同値であり、解は元の「回路が 1 を出力する入力を見つける」問題の解でもある。逆に、SAT が Circuit-SAT に還元可能であることは、ブール論理式を回路として書き直して解くことによって自明に従う。

関連項目

• テンプレート:仮リンク
• 充足可能性問題