充足可能性問題

出典: フリー百科事典『ウィキペディア（Wikipedia）』

充足可能性問題（じゅうそくかのうせいもんだい、satisfiability problem, SAT）は、一つの乗法標準形 (CNF) が与えられたとき、それに含まれるすべての変数の値を偽 (False) あるいは真 (True) にうまく定めることによって全体の値を'真'にできるか、という問題をいう。

目次

[編集] 定義

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

  • リテラル -- 論理変数 (x_1)\, またはその否定 (\bar{x_1})
  • クロージャ -- リテラルの論理和 (x_1 \lor \bar{x_2} \lor ...)

[編集] 問題

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

[編集] 例題

  • (x_1 \lor x_2) \land (x_1 \lor \bar{x_2}) \land (\bar{x_1} \lor \bar{x_2})
x1=真, x2=偽, を代入すると論理式は真になる。よって解答はYes。
  • (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})
x1, x2, いかなる真偽値を代入しても論理式は偽になる。よって解答はNo。

[編集] NP完全

充足可能性問題はNPかつNP困難な問題である。このような問題のクラスをNP完全問題という。充足可能性問題を多項式時間で変形することによって、様々なNP完全問題を構成することができる。

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

  • CNF-SAT -- クロージャの論理積からなるもの。
  • 3-SAT -- CNF-SATのうち、クロージャ内のリテラル数が、高々3つのもの。

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

[編集] 関連項目

"http://ja.wikipedia.org/wiki/%E5%85%85%E8%B6%B3%E5%8F%AF%E8%83%BD%E6%80%A7%E5%95%8F%E9%A1%8C" より作成