充足可能性問題

充足可能性問題（SAT）とは

充足可能性問題（SAT: satisfiability problem）とは、与えられた命題論理式に対して、その論理式全体を「真」にするような変数の真偽値の組み合わせが存在するかどうかを判定する問題です。

定義

SATを理解するために、まず以下の要素を定義します。

論理変数:
真(True)または偽(False)の値を取る変数。例：x₁, x₂, ...
論理演算子:
否定 (¬): ¬x₁ は、x₁が真の時偽、偽の時真となる。
論理和 (∨): x₁ ∨ x₂ は、x₁またはx₂が真の時真、両方偽の時偽となる。
論理積 (∧): x₁ ∧ x₂ は、x₁かつx₂が真の時真、それ以外は偽となる。
リテラル:
論理変数(x₁)またはその[否定]のこと。
節:
リテラルの論理和。例：(x₁ ∨ ¬x₂ ∨ ...)

問題

与えられた論理式が、上記の要素を用いて構成されているとき、その論理式全体を真にするような論理変数への真偽値の割り当てが存在するかを判定するのがSATです。

例題

例1：充足可能な場合


(x₁ ∨ x₂) ∧ (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ ¬x₂)


この論理式は、x₁=真、x₂=偽とすると全体が真となるため、充足可能です。

例2：充足不可能な場合


(x₁ ∨ x₂) ∧ (¬x₁ ∨ x₂) ∧ (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ ¬x₂)


この論理式は、どのような真偽値の割り当てをしても全体が真にならないため、充足不可能です。

NP完全性

充足可能性問題は、計算複雑性理論において重要な位置を占めています。

NP (非決定性多項式時間):
非決定性チューリングマシンで多項式時間で解ける問題のクラス。
NP困難:
NPに属する全ての問題を、多項式時間で解ける問題。
NP完全:
NPに属し、かつNP困難な問題。

SATは、NP完全問題の一例であり、他の多くのNP完全問題はSATに変換して解くことができます。これは、SATが計算の難しさの基準点として利用できることを示しています。

特殊な形式のSAT

CNF-SAT (連言標準形SAT):
節の論理積で表現されるSAT。例：(x₁ ∨ x₂) ∧ (x₁ ∨ ¬x₂)
3-SAT:
CNF-SATの中で、一つの節に含まれるリテラルの数が最大でも3つであるもの。3-SATもNP完全です。

co-NP問題

NP問題の補問題（Yes/Noを反転させた問題）をco-NP問題といいます。SATの補問題であるトートロジー判定問題（与えられた論理式が常に真となるかを判定する問題）は、co-NP完全です。

拡張

述語論理式にまで範囲を広げると、SATは決定不能となります。これは、ゲーデルの不完全性定理によって証明されています。

関連事項

数理論理学
NP完全問題
制約充足問題
デービス・パトナムのアルゴリズム
DPLLアルゴリズム
タブローの方法

もう一度検索