2-SATとは何か｜2点間の矛盾発見を多項式時間で検証する
2-SATとは、各節が2個以下のリテラルからなるCNF（Conjunctive Normal Form／連言標準形）の充足可能性問題である。Implication Graph（含意グラフ）と強連結成分（SCC／Strongly Connected Components）を用い、多項式時間で解ける。Pに属する。
3-SATや一般のCNF-SAT、3COL全体を2-SATへ還元できるわけではない。経営へ応用するなら、隣接する二者間の禁止条件・含意条件だけを二項射影として取り出し、局所Conflictを監視する手続である。全体問題を解いたことにはならない。
2-SATと3-SATの境界
| 問題 | 節幅 | 位置づけ |
|---|---|---|
| 2-SAT | 2以下 | P |
| 3-SAT | ちょうど3 | NP完全 |
| 一般SAT | 制限なし | NP完全 |
2-SATでは、節 (a ∨ b) を (¬a → b) かつ (¬b → a) という含意に直し、グラフの到達関係から矛盾を検出する。同じ変数 x と ¬x が同一SCCに入ればUNSAT（Unsatisfiable／充足不能）である。
例題：共有信号線上の左右ドライバ
ここでいうバスは、乗用車ではなく、複数の回路が同じ線を共有する信号線（共有ネット）を指す。変数を L（左ドライバが駆動）、R（右ドライバが駆動）とする。同時駆動禁止 (¬L ∨ ¬R) と、フローティング禁止 (L ∨ R) を置くと、割当は (L,R)=(1,0) または (0,1) に限られる。一方、「左右は常に同じ駆動状態」 (¬L ∨ R)、(¬R ∨ L) を足すと、同時駆動禁止と衝突し、L と ¬L が同一SCCに入って UNSAT になる。矛盾の有無を Yes/No で確認できる規模に留めることが要点である。
バリューチェーンの二項射影
実務では、バリューチェーンの隣接ペアから禁止条件を書く。
| 接続 | 監視する問い |
|---|---|
| 論理 → 知財 | 公理が知財を防御できるか |
| 知財 → 企画 | 模倣困難な表現へ落ちているか |
| 企画 → 調達 | コンセプトが調達思想に準拠するか |
| 調達 → 製造 | 素材が品質を具現化するか |
| 製造 → 流通 | 経路が価値を保存するか |
| 流通 → 販売 | 検証可能な体験を届けるか |
目的は全体最適化ではない。局所Conflictを安く早く露出させることである。
対話型証明との類似点
独立に生成された二つの回答・証跡をVerifierが照合する設計は、2証明者対話の着想に近い。証明者間の通信を許さず、相関する問いへの回答が二項制約を破らないかを見る。
全部を解かずに局所矛盾を高確率で露出させることが目的である。通過は「たぶん正しい」ではなく、「いま抜いた局所については矛盾が見つからなかった」という記録である。
チェックリスト
- 監視対象が二項制約に落ちているか
- 3リテラル以上の全体問題と混同していないか
- Implication GraphとSCCで矛盾を見ているか
- 局所通過を全体証明と書いていないか
- 値引きをreject破綻として扱えるか
2-SATの有効性は、難しい全体を簡単だと偽ることではなく、多項式時間で監視できる二項の層を切り出し、Conflictを先に洗う点にある。3-SATや3COLの全体充足を主張したいなら、別の手続と別の証跡が要る。
『P vs NP経営』の詳細はこちら https://link.amazon/B04IEdYsn