over 4 years ago

1.Model and Satisfiability

可滿足性(Satisfiability)是在探討, 邏輯式子所建立出的模型(Model),
可不可以找到一組解, 使得這個 Model 算出來的值可以是
例如:

則當 時,
Model Satisfiable
另一例子:

這種情形,不論 的值, 永遠都是
Model Unsatisfiable

2.Implementation 1

接著我們用nltk來做簡單的 Satisfiability 問題
先載入模組

>>> import nltk
>>> lgp = nltk.LogicParser()

接著,輸入邏輯式子

>>> p1 = lgp.parse('x | y')
>>> p2 = lgp.parse('-x | y')
>>> p3 = lgp.parse('x | -y')

然後把assignment加進去, 看看 是否 satisfiable

>>> val = nltk.Valuation([('x', True), ('y', True)])
>>> dom = val.domain
>>> g = nltk.Assignment(dom)
>>> m = nltk.Model(dom, val)
>>> m.satisfy(p1 & p2 & p3, g ) 
True

再把 加進去, 看看 是否 satisfiable

>>> p4 = lgp.parse('-x | -y')
>>> m.satisfy(p1 & p2 & p3 & p4, g ) 
False

3. First Order Logic

接著我們來看看如何將 ModelSatisfiability 的概念, 推廣到一階邏輯(First Order Logic)中
例如,在某個世界裡,
Gary 是個男生, Judy 是個女生, 而 Henry 是一隻狗,
GaryHenry 在跑步,
Judy 看見 HenryGary 看見 Judy
我們可以用一階邏輯(First Order Logic)把這個世界表示成一個 Model

根據這個Model, 用Satisfiability的概念, 可以求解以下問題
1 . 找找看這個世界中女生有哪些
這個問題可以看成是, 從找 M 中找出滿足 值有哪些,
可求解 Satisfiability , 得出:
女生有 Judy , 因為當 時, Satisfiable

2 . 回答這個世界中是否有男生在跑步, 或者, 是否有女生在跑步
這可以看成是, 判斷某個 formula 和這個 M 是否有交集, 得出:
有男生在跑步, 因為 中為 Satisfiable
沒有女生在跑步, 因為 中為 Unsatisfiable

3 . 回答是否 Judy 看見 Henry , 或者,是否 Judy 看見 Gary
可以判斷某個assignment 是否可讓 MSatisfiable , 得出:
Judy 看見 Henry , 因為當 時, 中為 Satisfiable
Judy 沒有看見 Gary , 因為當 時, 中為 Unsatisfiable

註:
1.在 python nltk 用的是 Closed World Assumption
也就是說, 在 Model 裡面沒有定義的, 一律為 False
例如沒有定義 Run(j) , 所以 Run(j)False
因此 中為 Unsatisfiable
同理, See(j,g) 中為 Unsatisfiable

2.相對於 Closed World Assumption
有另一種叫作 Open World Assumption
是將沒有定義的formula 它視為 Unknown
所以結果除了 TrueFalse 之外, 還有 Unknown

4.Implementation 2

用 python nltk 來實作看看:
首先, 建立 model

>>> v = """ 
... Gary => g
... Judy => j
... Henry => h
... boy => {g}
... girl => {j}
... dog => {h}
... run => {g, h}
... see => {(j, h), (g, j), (g, h)}
... """
>>> val = nltk.parse_valuation(v)
>>> m = nltk.Model(val.domain, val)

1.求 值:

>>> m.satisfiers(lgp.parse('girl(x)'), 'x'  , nltk.Assignment(val.domain, []))
set(['j'])

得出結果

2.求 這兩個formula在 中是否為 Satisfiable

>>> m.satisfy(lgp.parse('exists x.(run(x) & boy(x))'),nltk.Assignment(val.domain, []))
True
>>> m.satisfy(lgp.parse('exists x.(run(x) & girl(x))'),nltk.Assignment(val.domain, []))
False

得出結果:
中為 Satisfiable
中為 Unsatisfiable

3.求 對於 中是否為 Satisfiable

>>> m.satisfy(lgp.parse('see(x,y)'),nltk.Assignment(val.domain,[('x', 'j'), ('y', 'h')]))
True
>>> m.satisfy(lgp.parse('see(x,y)'),nltk.Assignment(val.domain,[('x', 'j'), ('y', 'g')]))
False

得出結果:
時, 中為 Satisfiable
時, 中為 Unsatisfiable

5.Reference

關於python nltk的 modelsatistiability 可參考:
http://nltk.googlecode.com/svn/trunk/doc/book/ch10.html

關於 Closed World AssumptionOpen World Assumption 可參考:
http://en.wikipedia.org/wiki/Closed_world_assumption
http://en.wikipedia.org/wiki/Open_world_assumption

← 自然語言處理 -- Ngram Smoothing / Interpolation Python Standard Library -- difflib →
 
comments powered by Disqus