充足可能性問題

Boolean Satisfability 略して SAT

試験の SAT と被るのでググるのに苦労しがち

与えられた bool 論理式を True にする変数割当は存在するか？という問題

例

$ a\lor bは$ (a,b)=(\rm{True}, \rm{False})の時に$ \rm Trueなので充足可能

$ a\land\lnot aは何を割り当てても $ \rm{False} なので充足不能

難しい問題の代表例

NP完全性が証明された初めての問題 (Cook-Levin theorem)

証明方法は、非決定的チューリングマシンのルールと動作を論理式で再現するというドストレートなもの

各時刻の状態やテープの各セルに対応する変数をチューリングマシンのルールで制約する

充足可能な場合はその時の変数の値が、各時刻の状態やテープの各セルの値ということになる

任意の論理式を CNF に多項式時間で変換でき、 CNF の方が扱いやすい

このため充足可能性問題と言うと普通は CNF に対するものを言う