充足可能性問題【satisfiability problem】SAT

充足可能性問題とは？

与えられた論理式に対し、各変数へ真偽値を割り当てることで式全体を真にできるかどうかを判定する問題。論理回路やプログラム検証などの分野で扱われ、計算量理論において重要な基準問題として知られる。

論理式は、複数の変数と「AND」（かつ）、「OR」（または）、「NOT」（～ではない）などの論理演算子で構成される。このとき、例えば「（ A OR NOT B ） AND （ NOT A OR C）」のような式が与えられたとき、A・B・Cにどのような真偽値を割り当てれば式全体が真になるか、あるいは、そのような割り当てが存在しないかを調べるのが充足可能性問題である。

変数の数が増えると、調べるべき組み合わせは指数関数的に膨れ上がる。変数が10個あれば2の10乗、すなわち1024通りの組み合わせを検討する必要がある。現在のところ、どんな論理式でも効率よく解を求めることができるアルゴリズムは発見されておらず、総当たり探索に頼らざるを得ない。

充足可能性問題は1971年にスティーブン・クック（Stephen A. Cook）によって「NP完全」問題であることが証明された。NP完全とは、「解の正しさは素早く確認できるが、解を素早く見つける方法が知られていない」問題のクラスである。NP完全に属する問題はすべて互いに変換可能であるため、充足可能性問題が効率よく解けるなら、他のNP問題もすべて効率よく解けることになる。これは「P≠NP問題」と呼ばれるコンピュータ科学最大の未解決問題と直結している。

実用面では、充足可能性問題を高速に解こうとする「SATソルバー」と呼ばれるプログラムが開発されており、回路設計の検証やソフトウェアのバグ検出、人工知能の推論処理など、幅広い分野で活用されている。理論上は困難な問題であっても、実際の問題に現れる論理式には構造的な規則性があることが多く、SATソルバーはその性質を巧みに利用して現実的な時間で解を導き出している。