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
接著我們來看看如何將 Model 和 Satisfiability 的概念, 推廣到一階邏輯(First Order Logic)中
例如,在某個世界裡,
Gary 是個男生, Judy 是個女生, 而 Henry 是一隻狗,
Gary 和 Henry 在跑步,
Judy 看見 Henry 而 Gary 看見 Judy
我們可以用一階邏輯(First Order Logic)把這個世界表示成一個 Model：
根據這個Model, 用Satisfiability的概念, 可以求解以下問題
1 . 找找看這個世界中女生有哪些
這個問題可以看成是, 從找 M 中找出滿足 的 值有哪些,
可求解 的 Satisfiability , 得出：
女生有 Judy , 因為當 時, 為 Satisfiable
2 . 回答這個世界中是否有男生在跑步, 或者, 是否有女生在跑步
這可以看成是, 判斷某個 formula 和這個 M 是否有交集, 得出：
有男生在跑步, 因為 在 中為 Satisfiable
沒有女生在跑步, 因為 在 中為 Unsatisfiable
3 . 回答是否 Judy 看見 Henry , 或者,是否 Judy 看見 Gary
可以判斷某個assignment 是否可讓 M 為 Satisfiable , 得出：
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
所以結果除了 True 和 False 之外, 還有 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的 model 和 satistiability 可參考：
http://nltk.googlecode.com/svn/trunk/doc/book/ch10.html
關於 Closed World Assumption 與 Open World Assumption 可參考：
http://en.wikipedia.org/wiki/Closed_world_assumption
http://en.wikipedia.org/wiki/Open_world_assumption
