命題論理

認知システム論知識と推論（２）
知識と論理で問題を解決する
充足可能性問題SAT
(Satisfiability Problem)
節と連言標準形
Davis-Putnumのアルゴリズム
復習：命題論理の論理式
論理式：原始命題を論理記号でつないだ文．
論理式
論理定数は論理式である．
true false
命題記号は論理式である．
p
P が論理式ならば， (P ) は論理式である．
P が論理式ならば，以下の４つも論理式である．
( P  Q) ( P  Q) ( P  Q) ( P  Q)
復習：論理式の解釈と意味
p,q,.. の解釈を決めると，他の論理式の解釈は：
true の値はT（真）， false の値はF（偽）
命題変数
(P ) の値は P の値の逆．
( P  Q) ( P  Q) ( P  Q) ( P  Q)
の値は，以下の真理値表に基づいて決める．
P
Q
P∧Q
P∨Q
P→Q
P Q
T
T
T
T
T
T
T
F
F
T
F
F
F
T
F
T
T
F
F
F
F
F
T
T
復習：恒真，充足不能，充足可能
恒真どんな解釈のもとでも真
例
( P  ( P  Q))  Q
充足不能どんな解釈のもとでも偽
例
P  P
充足可能ある解釈のもとで真
例
P Q
本日の主役！
充足不能
充足可能
P  P
P Q
本日の主役！
恒真
( P  ( P  Q))  Q
復習：論理的帰結
論理的帰結
P1, P2 ,
Q
, Pn
のすべてを真とするどんな解釈のもとでも
が真
Q
は
P1, P2 ,
P1  P2 
, Pn
の論理的帰結
 Pn  Q
が恒真
本日の主役！
P1  P2 
 Pn  Q
が充足不能
節と連言標準形
リテラル，節，連言標準形
Literal
リテラル
p
p
命題記号はリテラルである．
 命題記号
p  q  r
はリテラルである．
正リテラル
負リテラル
Clause
節
リテラルの選言(orで結合したもの）
p  q  r
( p  q)  ( p  q)  r
連言標準形(CNF)
Conjunctive Normal Form
節の連言(andで結合したもの）
( p  q)  ( p  q)  r
連言標準形(CNF)への変換
どんな論理式も以下の変換ルール（左辺を右辺に書換え）で
等価なCNFに変換できる．
CNFへの変換
1
2
3
4
5
6
P  Q  ( P  Q)  (Q  P)
P  Q  P  Q
P  P
( P  Q)  (P)  (Q)
( P  Q)  (P)  (Q) ド・モルガンの法則
( P  Q)  R  ( P  R)  (Q  R) 分配則
CNFへの変換
例
p   (q  r )
 p   ( q  r )
  p   ( q  r )
  p  ( q   r )
  p  (q   r )
 ( p  q )  ( p   r )
CNF
したがって，つぎの２つの節が得られる．
節集合
 pq
 p  r
節と if-then ルール
節は if-then ルールに対応する．
pq 
p  q (if p then q)
負リテラルは条件の AND
 p  q  r

pq r
(if p & q then r )
正リテラルは結論の OR
 p  q  r  s

pq rs
節と if-then ルール（特殊ケース）
true は∧(and)の単位元:
true  x  x
⇒ n=0 のとき： x1 
false は∨(or)の単位元：
⇒ n=0 のとき：
 xn  true
false  x  x
x1 
 xn  false
p  q  true  p  q
 p   q  p  q  false
 true  false 
（空節は矛盾を表す）
false
Davis-Putnumのアルゴリズム
Davis-Putnam のアルゴリズム(DPLL)
【入力】節集合S （CNFの命題論理式）
【出力】 Sの充足可能性を有限時間で判定する．
– 充足可能ならば true を返す．
– 充足不能ならば false を返す．
【手順】以下の３つのヒューリスティクスを用いて探索木の枝刈
りをしながら，Sを充足する解釈（モデル）をバックトラック法で
網羅的に探索する．
– 早期の停止判定ヒューリスティクス
– 純リテラルヒューリスティクス
– 単位節ヒューリスティクス
入力形式の例
変数の数
変数の数 x1,…,x100
x1,…,x100
100 427
-71 -64
24
41 -93 -54
73 81 54
-37 -32
73
-69 -39
-8
70
80
29
4
69
37
………………….
節の数
0
0
0
0
0
0
0
￢X71∨￢X64∨X24
分岐規則（バックトラック法による探索）
節集合 S 中の変数シンボルを L とする．
S が充足可能
•L = true に割り当てた場合
•L = false に割り当てた場合
のいずれかが充足可能
バックトラック法で探索
早期の停止判定ヒューリスティクス
x1  true, x2  false
リテラルが１つでも true である節は true
true
x1  x2  x3
節が１つでも false である節集合は false
false
x1  x2  x3  falseのリテラルは削除する

x1  x2
 = false

x1  x3

純シンボルヒューリスティクス(1/2)
純シンボル＝同じ符号（正／負）でしか現れない変数シンボル
正の純シンボル
A = true とする
負の純シンボル
B = false とする
 A  B 


 B  C 
C  A 


充足性判定のためには，純シンボルが true になるような
値の割り当てだけを考慮すれば十分である．
純シンボルヒューリスティクス(2/2)
アルゴリズムは，すでに true である節を無視する
B  false
true
A  B  C
A  C
負の純シンボル
A = false とする
正の純シンボル
C = true とする
単位節ヒューリスティクス
単位節＝１つのリテラルだけからなる節
A
B
DPLLアルゴリズムでの単位節の定義：
１つのリテラル以外にすべて false が割り当てられた節
A  true, B  false
A  B  C
単位節
C = true とする
充足性判定のためには，単位節を構成するリテラルが true
になるような値の割り当てだけを考慮すれば十分である．
単位節伝播(unit propagation)
単位節ヒューリスティクスによってリテラルの値を決めると，
さらに単位節が生じて，単位節ヒューリスティクスを連続的
に使用できることがある．
A  true
true
true
true
A  B
 B  true
B  C  C  false
 D  true
CD
DPLLアルゴリズムのメインプログラム
節集合
変数シンボルの集合
boolean DPLLmain (S, V) {
return DPLL (S, V, [ ] );
}
変数シンボルへの
空の割り当て
DPLLアルゴリズム
節集合
boolean DPLL (S, V, I) {
変数シンボルの集合
if (すべての節が真) return true
if (ある節が偽) return false
p, value ← 純シンボルとその値を探す
変数シンボルへの
真偽値の割り当て
（解釈）
割当て (p = value)
をＩに追加
if (p≠null) return DPLL(S, V-{p}, extend(p, value, I))
p, value ← 単位節を探す
if (p≠null) return DPLL(S, V-{p}, extend(p, value, I))
p ←Vのうちの1つのシンボル
return DPLL (S, V-{p}, extend(p, true, I)) or
DPLL (S, V-{p}, extend(p, false, I))
}
例題魔宮の世界(1/2)
背景知識
(1,2) にモンスターがいるなら，(1,1) で異臭を感じる
M 12  S11
M12  S11
(1)
(1,2) に落とし穴があるなら，(1,1) で風を感じる
P12  B11
P12  B11
(2)
(1,2) にモンスターも落とし穴もないなら，(1,2) はOK
(3)
M 12  P12  OK12 M12  P12  OK12
事実
(1,1) で異臭を感じない
S11
(4)
(1,1) で風を感じない
B11
(5)
質問
(1,2) はOKか？
OK12
(6)
例題魔宮の世界(2/2)
false
M12  S11
(1)
P12  B11
(2)
M12  P12  OK12
true
S11
true
true
true
true
(3)
(4)
B11
(5)
OK12
(6)
単位節(4) S11=false
単位節(1) M12=false
単位節(5) B11=false
単位節(2) P12=false
空節(3) 充足不能
単位節(6) OK12=false
この例題の場合，分岐によるバックトラックは不要であった．

Download Report