さて、ようやくSATを説明する準備ができました。SATだけにさっと説明しましょう。
【充足問題(SAT)】
いま、Uをブール変数の集合とします。
かつ、集合CはU上の節の有限集合。
このとき、Cを充足する真理関数が
存在するかどうかを決定する問題を
充足問題(SAT)と言います。
SATの結果はyesかnoで表わされます。
例を竹内外史先生の同じく「PとNP」p.11から挙げましょう。竹内先生の例は難しいですが解くと大変役に立ちます。解説はその下に書きますので、自分で解こうと思う方は読まないようにして下さい。
例
ブール変数の集合Uがいま、U={u1,u2}で表せるとき
C={{u1,¬u2}{¬u1,u2}}とすればCの充足問題はyesである。
すなわちt(u1)=t(u2)=Tまたはt(¬u1)=t(¬u2)=Tのとき。
しかし、C={{u1,u2}{¬u1},{¬u2}}ならばCの充足問題は
noである
解説
真理関数は、すべての節のどれかの元を満たす
必要があります。
節を、論理記号に展開して真理値表というもの
を書いてみると分かりやすいと思います。
真理値表というのは、例を挙げれば簡単で
論理和の真理値表は、論理和が項を2つ持つ
演算であるからその項のすべての値の
組み合わせと、結果を表にしたものです。
これだとA∨Bの値がFになるのはA=B=Fの時のみ
というのが一目で分かりますね
言い方を変えれば節の集合{{A,B}}を
充足するような真理関数tは、
t(A)=T,t(B)=T
の2つがありますね。
真理関数は節の中のいずれかの元でTになれば
いいのでした。そして、いま節集合の元は1つ
ですから、これで十分です。
では、上記の例について考えてみましょう
a) C={{u1,¬u2}{¬u1,u2}}の場合
(u1∨¬u2)∧(¬u1∨u2)と同じ意味ですから、
この論理式の真理値表を書いてみると、
従って、節集合C={{u1,¬u2}{¬u1,u2}}を
充足する真理関数は、
t(u1)=t(u2)=T, t(¬u1)=t(¬u2)=T
の二つがあります。なんか、変な感じですが、
真理関数は、節の元のうち一つのリテラルしか
対応しないのでこうなると思って下さい。
従って、SATとしては、yesが結果となります。
b) C={{u1,u2}{¬u1},{¬u2}}の場合
(u1∨u2)∧¬u1∧¬u2と同じ意味ですから、
この論理式の真理値表を書いてみると、
というか、見るまでもなくなのですが、
一応書いてみると、
となります
したがって、節集合C={{u1,u2}{¬u1},{¬u2}}を
充足する真理関数はなく、SATの答えはno
となります。
結局、SATは、節集合を論理式として表わしたときにTとなるようなリテラルの組があるかどうか、という問題に表せるようですね。それならそうと言えば、それこそさっと済むものなのに(笑い)
0 件のコメント:
コメントを投稿
Etsuro.Honda@futarisizuka.org