充足可能性問題

【じゅうそくかのうせいもんだい (satisfiability problem)】

真または偽を表す論理変数とそれらの否定からなる和積形論理式, 例えば$(x_{1}\lor {\bar {x}}_{2}\lor x_{3})\land ({\bar {x}}_{1}\lor {\bar {x}}_{3})\land (x_{2}\lor {\bar {x}}_{3})\,$が与えられているとき, この式が真になるような論理変数への割り当てが存在するとき充足可能といい, それを判定する問題をいう. クック (Cook) が1971年にNP完全性を示した最初の問題. デイビス・プットナム (Davis-Putnam) のアルゴリズムなどが知られている. 以上は命題論理における充足可能性問題であるが, 述語論理における充足可能性問題は決定不能である.