充足可能性問題

充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの命題論理式が与えられたとき、それに含まれる変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。

定義

真偽値をとる論理変数 ${\displaystyle \textstyle {x_{1},x_{2}\dots }}$ および論理演算子により論理式を構成する。

• 論理否定 ${\displaystyle ({\bar {x_{1}}})\dots x_{1}}$ が真ならば偽 偽ならば真
• 論理和 ${\displaystyle (x_{1}\lor x_{2})\dots x_{1}}$ が真ならば ${\displaystyle x_{1}\,}$ 偽ならば ${\displaystyle x_{2}\,}$
• 論理積 ${\displaystyle (x_{1}\land x_{2})\dots x_{1}}$ が真ならば ${\displaystyle x_{2}\,}$ 偽ならば${\displaystyle x_{1}\,}$
• リテラル - 論理変数 ${\displaystyle (x_{1})\,}$ またはその否定 ${\displaystyle ({\bar {x_{1}}})}$
• 節 - リテラルの論理和 ${\displaystyle (x_{1}\lor {\bar {x_{2}}}\lor ...)}$

問題

論理式全体の値を真にするような、真偽値 ${\displaystyle x_{1},x_{2}\dots }$ の組み合わせは存在するか？

例題

• ${\displaystyle (x_{1}\lor x_{2})\land (x_{1}\lor {\bar {x_{2}}})\land ({\bar {x_{1}}}\lor {\bar {x_{2}}})}$

x₁=真, x₂=偽, を代入すると論理式は真になる。よって解答はYes。

• ${\displaystyle (x_{1}\lor x_{2})\land ({\bar {x_{1}}}\lor x_{2})\land (x_{1}\lor {\bar {x_{2}}})\land ({\bar {x_{1}}}\lor {\bar {x_{2}}})}$

x₁, x₂, いかなる真偽値を代入しても論理式は偽になる。よって解答はNo。

NP完全

充足可能性問題はNP（Non-deterministic Polynomial time（非決定性多項式時間）非決定性チューリングマシンによって多項式時間で解くことができる問題）かつNP困難な問題である。このような問題のクラスをNP完全問題という。充足可能性問題を多項式時間で変形することによって、様々なNP完全問題を構成することができる。

任意の論理式からなる充足可能性問題はNP完全であるが、ある特殊な形状をもつ論理式のクラスに限定しても、なおNP完全であることが証明されている。

• CNF-SAT - 節の論理積からなるもの。

• 3-SAT - CNF-SATのうち、節内のリテラル数が、高々3つのもの。

NP問題の補問題、つまり結果のYesとNoを逆転させた問題をco-NP問題という。

充足可能性問題のYesとNoを逆転させ、論理式に否定をかけて変形すると、トートロジー判定問題になる。トートロジー判定問題はco-NP完全問題である。

拡張

論理式の範囲を述語論理式に拡大した場合、ゲーデルの不完全性定理により、充足可能性問題は決定不能である。 平たくいえば、もし述語論理の充足可能性問題が決定可能であるならば、その方法を利用して自然数論によるそれ自身の無矛盾性証明が可能となるが、それは不完全性定理により否定されるからである。

関連項目

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