充足可能性問題

提供: miniwiki
移動先:案内検索

充足可能性問題(じゅうそくかのうせいもんだい、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]
x1=真, x2=偽, を代入すると論理式は真になる。よって解答は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]
x1, x2, いかなる真偽値を代入しても論理式は偽になる。よって解答は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完全問題である。

関連項目