充足可能性問題SAT (Satisfiability Problem)

Presentation on theme: "充足可能性問題SAT (Satisfiability Problem)"— Presentation transcript:

1 充足可能性問題SAT (Satisfiability Problem)
認知システム論　知識と推論（２） 知識と論理で問題を解決する 充足可能性問題SAT (Satisfiability Problem) 　節と連言標準形 　Davis-Putnumのアルゴリズム 　ある命題が与えられた知識ベースの論理的帰結かどうかは，演繹（えんえき）定理によって，知識ベースに命題の否定を追加してできる論理式が充足不能かどうかに帰着する．そして，充足不能性の判定は，ちょうどその裏の概念である充足可能性の判定に帰着する．論理式の命題論理式が充足可能かどうかを判定する問題は，充足可能性問題(SAT）と呼ばれており，コンピュータサイエンスや人工知能において重要な役割を果たしている．今回はSATの正確な定義およびそれを解くアルゴリズムを学ぶ． 　まず，論理式を連言標準形という簡単な形に変形し，節と呼ばれる簡単な論理式の集合によって表現する方法を学ぶ．そして，節集合として与えられた論理式が充足可能かどうかを判定する Davis-Putnum のアルゴリズムを学ぶ．

2 復習：命題論理の論理式 論理式 論理定数 は論理式である． true false 命題記号 は論理式である．
論理式： 原始命題を論理記号でつないだ文． 論理式 論理定数　は論理式である． true false 命題記号　は論理式である． が論理式ならば，　　　　 　　は論理式である． が論理式ならば，以下の４つも論理式である．

3 復習：論理式の解釈と意味 T F P Q P→Q P∨Q P∧Q Q P « 命題変数 p,q,.. の解釈を決めると，他の論理式の解釈は：
true の値はT（真）， false の値はF（偽） 　　　 　　　　の値は　　の値の逆． 　の値は，以下の真理値表に基づいて決める． T F P　 Q P→Q P∨Q P∧Q Q P

4 復習：恒真，充足不能，充足可能 恒真 どんな解釈のもとでも真 例 充足不能 どんな解釈のもとでも偽 例 充足可能 ある解釈のもとで真
恒真　どんな解釈のもとでも真 例 充足不能　どんな解釈のもとでも偽 例 充足可能　ある解釈のもとで真 本日の主役！ 例 本日の主役！ 充足不能 充足可能 恒真

5 復習：論理的帰結 論理的帰結　 のすべてを真とするどんな解釈のもとでも が真 の論理的帰結　 は が恒真 本日の主役！ が充足不能

6 節と連言標準形

7 リテラル，節，連言標準形 リテラル 命題記号 はリテラルである． 正リテラル 命題記号 はリテラルである． 負リテラル 節
Literal リテラル 命題記号　はリテラルである． 正リテラル 　　命題記号　はリテラルである． 負リテラル Clause 節 リテラルの選言(orで結合したもの） Conjunctive Normal Form 連言標準形(CNF) 　１個の命題記号そのもの，または，その否定をリテラルという．とくに，前者を正リテラル，後者を負リテラルという． 　リテラルの選言(orで結合したもの）を節という． 　節の連言(andで結合したもの）を連言標準形（ＣＮＦ）という． 　したがって，ＣＮＦでは最も外側では and 記号が現れて節を結合しており，各節の内部では or 記号がリテラルを結合し，リテラルの内部では not 記号が現れるというように，and, or, not が整然とした入れ子構造の中に配置されている．論理式をこのような単純な形にすることによって，それを処理するさまざまなアルゴリズムを簡潔に記述することができる． 節の連言(andで結合したもの）

8 連言標準形(CNF)への変換 どんな論理式も以下の変換ルール（左辺を右辺に書換え）で 等価なCNFに変換できる． CNFへの変換 1 2 3
4 ド・モルガンの法則 5 　論理式の形はかなり複雑なものになり得るが，その意味（真偽値）を変えることなく，それをＣＮＦに変換できる． 　論理式をＣＮＦに変換する方法は機械的である．このスライドに示されている６つの等式を用い，論理式の中にいずれかの等式の左辺に合致する部分があったら，それを対応する右辺に書き換える．そのような書換えを可能なだけ繰り返し，もうそれ以上書き換えられなくなったら，そのときの論理式はＣＮＦになっている． 　１つめの等式を使えば，同値記号を除去できる． 　２つめの等式を使えば，含意記号→を除去できる． 　この時点で論理記号は，not, and, or だけとなる． 　つぎに，４つめと５つめの等式（ド・モルガンの法則）を使うと，カッコ内のandやorを（orやandに）反転させながら外側に出し，notを論理式の内部に移動させることができる．notを最も内側まで移動すると，命題変数の直前にnotがついたもの，すなわち，リテラルができてくる． 　 ３つめの等式は，その途中でnot が連続した場合には，連続した２個を除去するものである． 　 ６つめの等式は，andがカッコの内側にあって， orがその外側にあるとき，分配則を適用して，orを内側にし，andを外側にするものである．これを繰り返すとすべてのandが最も外側に来て，その内側はorによりリテラルを結合したもの，すなわち，節となる． 分配則 6

9 CNFへの変換 例 CNF したがって，つぎの２つの節が得られる． 節集合
　これがその例題．最初に与えられた論理式がどの等式によって書き換えられているかを確認してほしい． 　ＣＮＦに含まれる節の集合を節集合という．節集合に含まれる節は，暗黙裏に，andで結合されているので，すべてが「真」であると解釈される．人工知能の応用において，多くの場合，知識ベースは節集合としてモデル化されている． 節集合

10 節と if-then ルール 節 は if-then ルールに対応する． 正リテラル は 結論 の OR 負リテラル は 条件 の AND
　「恒真」を説明したスライドで確認したように，節 ￢ｐ∨ｑ は，節 ｐ→ｑと等価である． 　一般に，どのような節も，「もし○○かつ○○ならば，××または××である」というような if-then ルールというものと等価なものである． 　節は正リテラルと負リテラルを∨(or)で結合した論理式であるが，その中の負リテラルの否定記号（￢）を取り外したものが， if-then ルールの条件部（もし○○かつ○○ならば）にきて，それらがすべて∧(and)で結合される． 　一方，節の中のすべての正リテラルは∨(or)で結合されたままif-then ルールの結論部（ ××または××である）になる．

11 節と if-then ルール（特殊ケース） true は∧(and)の単位元: ⇒ n=0 のとき： false は∨(or)の単位元：
　特殊ケースとして，節の中に負リテラルが１つもなければ， if-then ルールの条件部は true とする．また，節の中に正リテラルが１つもなければ， if-then ルールの結論部は false とする． 　その根拠は，and の単位元はtrue，or の単位元はfalse であることに基づく．andで結合されたn個の論理式には，暗黙に true も結合されていると考えてよい．したがって，n=0のとき，その論理式は true である．また， orで結合されたn個の論理式には，暗黙に false も結合されていると考えてよい．したがって，n=0のとき，その論理式は false である． 　最後に，節が１つもリテラルを含まないものを空節というが，これはいまの約束を使えば，true → false （つまり，真ならば偽）となり，常に偽である論理式，あるいは，矛盾であることを表す論理式である． 　このような if-then ルールは，知識を論理的に表現するための言語の基本的な構文として使われることが多い． （空節は矛盾を表す）

12 休憩

13 Davis-Putnumのアルゴリズム

14 Davis-Putnam のアルゴリズム(DPLL)
【入力】　節集合S （CNFの命題論理式） 【出力】　Sの充足可能性を有限時間で判定する． 充足可能ならば true を返す． 充足不能ならば false を返す． 【手順】　以下の３つのヒューリスティクスを用いて探索木の枝刈りをしながら，Sを充足する解釈（モデル）をバックトラック法で網羅的に探索する． 早期の停止判定ヒューリスティクス 純リテラルヒューリスティクス 単位節ヒューリスティクス 　Davis, Putnam, Logemann, Loveland によって開発された充足可能性判定アルゴリズム DPLL を学ぶ． 　このアルゴリズムの入力，出力，および手順の概略はスライドにかかれているとおりである．

15 入力形式の例 変数の数 x1,…,x100 変数の数 x1,…,x100 節の数 100 427 -71 -64 24 0
…………………. ￢X71∨￢X64∨X24 　具体的には，入力はこのスライドのようなファイルに記述されていると考えるとよい．

16 分岐規則（バックトラック法による探索） 節集合 S 中の変数シンボルを L とする． S が充足可能 L = true に割り当てた場合
L = false に割り当てた場合 のいずれかが充足可能 　アルゴリズムの基本は，制約充足のところで学んだバックトラック法である．ある変数シンボル L に着目し，それを trueとするケースとfalseとするケースに分岐して探索する． 　すなわち，まず，それを true とするすべての解釈を探索し，すべての節を真にする解釈を１つでも見つけることができれば充足可能であることを示すのに成功したことになる． 　それに失敗した場合は，Lをfalseとするすべての解釈を探索し，すべての節を真にする解釈を１つでも見つけることができれば充足可能であることを示すのに成功したことになる．それにも失敗した場合は，充足不能である． バックトラック法で探索

17 早期の停止判定ヒューリスティクス = false リテラルが１つでも true である節は true true
節が１つでも false である節集合は false falseのリテラルは削除する = false false 　バックトラック法は，逐次的に変数シンボルに真または偽を割り当てていく．しかし，すべての変数に値を割り当てる前にも，つぎのようなことがわかるので，探索木の枝刈りなどに活用することができる． 　- リテラルが１つでも真である節は，真である．（節はリテラルを or で結合しているので．） 　逆に，リテラルが全部偽である節は偽であるが，その場合には，その節を含む節集合全体が偽となる． 　- 節が１つでも偽である節集合は，偽である．（節集合は節を and で結合しているので．）

18 純シンボルヒューリスティクス(1/2) 純シンボル＝同じ符号（正／負）でしか現れない変数シンボル 正の純シンボル 負の純シンボル
A = true とする 負の純シンボル B = false とする 　同じ符号（正／負）でしか現れない変数シンボルを純シンボル(pure symbol)という． 　正のリテラルとして現れる純シンボルには「真」を割り当てればよく，「偽」を割り当てる探索は不要であることが知られている．（「真」を割り当てた方が充足しやすい．「偽」を割り当てても充足しやすくなることはない．） 　同様に，負のリテラルとして現れる純シンボルには「偽」を割り当てればよく，「真」を割り当てる探索は不要である． 充足性判定のためには，純シンボルが true になるような 値の割り当てだけを考慮すれば十分である．

19 純シンボルヒューリスティクス(2/2) アルゴリズムは，すでに true である節を無視する true 負の純シンボル
A = false とする 正の純シンボル C = true とする 　DPLLアルゴリズムでは，「偽」を割り当てたリテラルや「真」となった節を，あたかも削除したかのように無視する．（「偽」が or の単位元，「真」が and の単位元であることによる．） 　したがって，このスライドの例のように，もともと AとC は純シンボルではないのだが，Bに偽を割り当てた後は，１つめの節は真なので，それが削除されたかのように無視すると，AとC は純リテラルということになる．

20 単位節ヒューリスティクス 単位節＝１つのリテラルだけからなる節
DPLLアルゴリズムでの単位節の定義： １つのリテラル以外にすべて false が割り当てられた節 単位節 C = true とする 　A や ￢B のように，１つのリテラルだけからなる節を単位節(unit clause)という． 　DPLLアルゴリズムでは，この定義をやや拡張して用い，１つのリテラル以外にすべて false が割り当てられた節を単位節という．これは１つ前のスライドで述べたように，「偽」であるリテラルは節から削除されたかのように無視すると思えば，もともとの定義と一致することから，その意味が理解できるでしょう． 　単位節があったら，そこに含まれる唯一のリテラルが「真」となるように変数シンボルに真偽を割り当てればよいことは自明でしょう．このスライドの例では，A=true, B=false を割り当てたとき，￢A∨B∨C は単位節(C)となるので，C=trueとする． 充足性判定のためには，単位節を構成するリテラルが true になるような値の割り当てだけを考慮すれば十分である．

21 単位節伝播(unit propagation)
単位節ヒューリスティクスによってリテラルの値を決めると， さらに単位節が生じて，単位節ヒューリスティクスを連続的に使用できることがある． true true true 　最初は単位節でなくても，単位節ヒューリスティクスによってリテラルの値を決めると，さらに単位節が生じて，単位節ヒューリスティクスを連続的に使用できることがある．このスライドの例では，もともとは単位節は１つもないのだが，いったんA=true という値を割り当てると，￢A∨B が単位節（B)となり，B=true となる．これがつぎつぎと他の節に波及して，C=false, D=true となる．これは制約充足で学んだ「制約伝播」に相当するもので，単位節伝播(unit propagation)と呼ばれている．

22 DPLLアルゴリズムのメインプログラム 節集合 変数シンボルの集合 boolean DPLLmain (S, V) {
return DPLL (S, V, [ ] ); } 変数シンボルへの 空の割り当て 　DPLLアルゴリズムの中心は，DPLLという再帰的関数である．メインプログラムでは，節集合S，すべての変数シンボルの集合V，および空の解釈（どの変数シンボルにも値を割り当てていない）を引数としてDPLLを呼び出している．

23 変数シンボルへの 真偽値の割り当て （解釈）
DPLLアルゴリズム 節集合 変数シンボルの集合 boolean DPLL (S, V, I) { if (すべての節が真) return true if (ある節が偽) return false p, value ← 純シンボルとその値を探す if (p≠null) return DPLL(S, V-{p}, extend(p, value, I)) p, value ← 単位節を探す p ←Vのうちの1つのシンボル return DPLL (S, V-{p}, extend(p, true, I)) or DPLL (S, V-{p}, extend(p, false, I)) } 変数シンボルへの 真偽値の割り当て （解釈） 割当て　(p = value) を　Ｉ　に追加 　再帰関数 DPLL は，３つの引数S，V，I を受け取る． 　S は節集合である．再帰呼び出しをしてもそのまま第１引数として引き継がれる普遍的なデータである． 　V は変数シンボルの集合である．ある変数pに真偽値を設定して再帰呼び出しするときに，Vからpが除去されたものを第２引数として渡す． 　I はこれまで設定した解釈（変数シンボルへの真偽値の割り当て）である．DPLLを再帰的に呼び出すときには，ある変数シンボル p に適切な真偽値 value を割り当てることによって，I を拡張したものを第３引数として渡す． 　DPLLは，解釈 I をさらに拡張することによってSを真にすることにできれば trueを返す．逆に，解釈 I をどのように拡張してもSを真にすることができないときは false を返す． 　アルゴリズムの内容はこれまで概説したとおりである． 　現在の解釈 I のもとですべての節が真ならば，適切な解釈を見つけたことになり，Sは充足可能であるので，DPLLは true を返す． 　現在の解釈 I のもとである節が偽ならば，I をどう拡張しても S は偽なので，DPLLは falseを返す． 　つぎに，純シンボルヒューリスティクスを適用する．純シンボルpが存在するならば，純シンボルヒューリスティクスによって定まるその真偽値をvalueとし，p=value を追加することによって解釈 I を拡張し，DPLLを再帰呼び出しする． 　純シンボルが存在しなければ，単位節ヒューリスティクスを適用する．単位節pが存在するならば，単位節ヒューリスティクスによって定まるその真偽値をvalueとし， p=value を追加することによって解釈 I を拡張し，DPLLを再帰呼び出しする． 　純シンボルも単位節も存在しなければ，探索木を探索する．あるシンボルpを選び，まずそれに真を割り当て，p=trueを追加することによって解釈 I を拡張し，再帰呼び出しをする．その戻り値が true なら，p=true という割り当てが成功してSのすべての節を真とすることができたことになるので，その戻り値 trueをそのまま返す．再帰呼び出しの戻り値が falseなら，プログラミング言語の or の機能によって，こんどはpに偽を割り当て， p=falseを追加することによって解釈 I を拡張し，再帰呼び出しする．そこからの戻り値が true/false のいずれであれ，それが最終的にこの関数からの戻り値になる． 　プログラミング上のコメント：上記のような制御は２つのDPLL呼び出しを結合している or によってなされている．一般に，P or Q （CやJavaでは，P || Q）は，逐次的ORと呼ばれており，必ずしもPとQの両方を実行するわけではない．Pがtrueならば，Qを実行せずにtrueを返し，Pがfalseならば，Qを実行してその値を返す．

24 例題 魔宮の世界(1/2) 背景知識 (1,2) にモンスターがいるなら，(1,1) で異臭を感じる
例題　魔宮の世界(1/2) 背景知識 (1,2) にモンスターがいるなら，(1,1) で異臭を感じる (1,2) に落とし穴があるなら，(1,1) で風を感じる (1,2) にモンスターも落とし穴もないなら，(1,2) はOK 事実 質問 (1,1) で異臭を感じない (1,2) はOKか？ 　前回学んだ魔宮の世界の例題の一部についての例題である． 　背景知識に含まれる３つの if-then ルールを節として表現したものを(1),(2),(3)とする． 　事実を表す(4),(5)はすでに節（単位節）となっている． 　調べたいことは(1,2)が安全であること，すなわち，OK12が(1)-(5)の論理的帰結であることである．それを確認するために，その否定(6)を付け加えて，(1)-(6)が全体として充足不能であることを調べることとする． (1,1) で風を感じない

25 例題 魔宮の世界(2/2) true true false true true true 単位節(4) S11=false
例題　魔宮の世界(2/2) true true false true true true 単位節(4)　S11=false 単位節(1)　M12=false 　このスライドで示されているように，この例題の場合，分岐によるバックトラックすることなしに，(1)-(6)が充足不能であることを確認することができる．ゆえに，演繹定理より，OK12 は背景知識と事実の論理的帰結である． 単位節(5)　B11=false 単位節(2)　P12=false 単位節(6)　OK12=false 空節(3)　充足不能 この例題の場合，分岐によるバックトラックは不要であった．