充足可能性問題のソースを表示

{{Expand English|Boolean satisfiability problem|date=2024-04}}
{{出典の明記| date = 2023年11月}}
'''充足可能性問題'''（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの[[命題論理|命題論理式]]が与えられたとき、それに含まれる[[変数 (数学)|変数]]の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。SATisfiabilityの頭3文字を取ってしばしば「SAT」と呼ばれる。

==定義==

[[真偽値]]をとる論理変数 <math>\textstyle{x_1, x_2 \dots}</math> および[[論理演算子]]により論理式を構成する。
*[[否定|論理否定]] <math>(\bar{x_1}) \dots x_1</math> が真ならば偽 偽ならば真
*[[論理和]] <math>(x_1 \lor x_2) \dots x_1</math> が真ならば <math>x_1\,</math> 偽ならば <math>x_2\,</math>
*[[論理積]] <math>(x_1 \land x_2) \dots x_1</math> が真ならば <math>x_2\,</math> 偽ならば<math>x_1\,</math>
*[[リテラル]] - 論理変数 <math>(x_1)\,</math> またはその否定 <math>(\bar{x_1})</math>
*節 - リテラルの論理和 <math>(x_1 \lor \bar{x_2} \lor ...)</math>

== 問題 ==
論理式全体の値を真にするような、真偽値 <math>x_1, x_2 \dots</math> の組み合わせは存在するか？

=== 例題 ===
*<math>(x_1 \lor x_2) \land (x_1 \lor \bar{x_2}) \land (\bar{x_1} \lor \bar{x_2})</math>
:x<sub>1</sub>=真, x<sub>2</sub>=偽, を代入すると論理式は真になる。よって解答はYes。

*<math>(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})</math>
:x<sub>1</sub>, x<sub>2</sub>, いかなる真偽値を代入しても論理式は偽になる。よって解答は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アルゴリズム]]
* [[タブローの方法]]

{{デフォルトソート:しゆうそくかのうせいもんたい}}
[[Category:数学基礎論]]
[[Category:形式手法]]
[[Category:数学の問題]]
[[Category:数学に関する記事]]