1、12.4 可滿足性問(wèn)題與消解法q可滿足性問(wèn)題：可滿足性問(wèn)題：q用于證明用于證明A是否永真是否永真q用于驗(yàn)證邏輯蘊(yùn)涵用于驗(yàn)證邏輯蘊(yùn)涵qA1Ak B 永真永真 當(dāng)且僅當(dāng)當(dāng)且僅當(dāng) A1Ak B 永假永假q解決方法解決方法q真值表真值表q主析取范式主析取范式q主合取范式主合取范式q缺陷：計(jì)算量大缺陷：計(jì)算量大22.4 可滿足性問(wèn)題與消解法q無(wú)論是命題演算還是謂詞演算，自然推理系統(tǒng)無(wú)論是命題演算還是謂詞演算，自然推理系統(tǒng)是比較便于使用的，但對(duì)于計(jì)算機(jī)實(shí)現(xiàn)來(lái)說(shuō)，是比較便于使用的，但對(duì)于計(jì)算機(jī)實(shí)現(xiàn)來(lái)說(shuō)，仍然過(guò)于復(fù)雜。仍然過(guò)于復(fù)雜。 q消解法消解法32.4 可滿足性問(wèn)題與消解法q 分離規(guī)則q 可改為q q 闡

2、明：q 該規(guī)則要求“消去兩個(gè)互補(bǔ)文字”。q “操作特征q 對(duì)第二種形式作如下的推廣：q qqpp,qqpp,（1）mnmnrrqqrrpqqp.,.111142.4 可滿足性問(wèn)題與消解法q設(shè)設(shè)C1，C2為兩個(gè)簡(jiǎn)單析取式，稱為子句，為兩個(gè)簡(jiǎn)單析取式，稱為子句，L1，L2是分別屬于是分別屬于C1，C2的互補(bǔ)文字對(duì)，用的互補(bǔ)文字對(duì)，用C-L表示表示從子句從子句C中刪除文字中刪除文字L后所得的子句，那么消解原后所得的子句，那么消解原理可表示為：理可表示為： q其中其中C1,C2稱為消解母式，稱為消解母式，L1，L2稱為消解基，稱為消解基，而而(C1-L1)(C2-L2)稱為消解結(jié)果。稱為消解結(jié)果。)2

3、2() 11(2, 1LCLCCC52.4 可滿足性問(wèn)題與消解法q例：設(shè)例：設(shè)C1為為RPQ，C2為為PQq以以P，P為消解基的消解結(jié)果是為消解基的消解結(jié)果是 RQQq以以Q，Q為消解基的消解結(jié)果是為消解基的消解結(jié)果是RPPq特別地，當(dāng)特別地，當(dāng)C1，C2都是單文字子句，且互補(bǔ)時(shí)，都是單文字子句，且互補(bǔ)時(shí)，C1，C2的消解結(jié)果不含有任何文字，這時(shí)我們稱的消解結(jié)果不含有任何文字，這時(shí)我們稱其消解結(jié)果是其消解結(jié)果是“空子句空子句”（nil），常用符號(hào)），常用符號(hào) 表示表示之之, 空子句空子句是永遠(yuǎn)無(wú)法被滿足的。是永遠(yuǎn)無(wú)法被滿足的。62.4 可滿足性問(wèn)題與消解法q定理定理1： 設(shè)設(shè)C是是C1，C2的

4、消解結(jié)果，那么的消解結(jié)果，那么C是是C1和和C2的邏輯結(jié)果。的邏輯結(jié)果。q闡明闡明q消解原理作為推理規(guī)則是適當(dāng)?shù)?。消解原理作為推理?guī)則是適當(dāng)?shù)摹作為特別情況，作為特別情況，p與與p的消解結(jié)果是的消解結(jié)果是 ， 實(shí)實(shí)質(zhì)上是質(zhì)上是pp的另一種表示形式的另一種表示形式,它們都是不可它們都是不可滿足的。滿足的。q給定一個(gè)合取范式給定一個(gè)合取范式S，S的所有簡(jiǎn)單析取式稱為的所有簡(jiǎn)單析取式稱為S的子句集。重復(fù)使用消解規(guī)則，可以的到一的子句集。重復(fù)使用消解規(guī)則，可以的到一個(gè)子句序列。個(gè)子句序列。72.4 可滿足性問(wèn)題與消解法q定義：定義： 設(shè)設(shè)S為一子句集，稱為一子句集，稱C是是S的消解結(jié)果，如的消解結(jié)果

5、，如果存在一個(gè)子句序列果存在一個(gè)子句序列C1，C2 ，,Cn（= C），），使使Ci(i = 1,2, ,n) q或者是或者是S中子句，中子句，q或者是或者是Ck，Cj (k,j i) 的消解結(jié)果。的消解結(jié)果。q該序列稱為是由該序列稱為是由S導(dǎo)出的導(dǎo)出的C的消解序列。的消解序列。q當(dāng)當(dāng)是是S的消解結(jié)果時(shí)，稱該序列為的消解結(jié)果時(shí)，稱該序列為S的一個(gè)否證的一個(gè)否證q（refutations）。）。82.4 可滿足性問(wèn)題與消解法q定理定理2：如果子句集：如果子句集S有一個(gè)否證，那么有一個(gè)否證，那么S是不可是不可滿足的。滿足的。q分析：設(shè)分析：設(shè)C1，C2 ，,Cn（= 是是S的一個(gè)否證的一個(gè)否證。若

6、。若S可滿足，即有某個(gè)賦值可滿足，即有某個(gè)賦值使使S中所有子句為中所有子句為真，那么可對(duì)真，那么可對(duì)n歸納證明，歸納證明，使使C1，C2 ，,Cn為真，從而為真，從而( Cn ) = () = 1，導(dǎo)致矛盾。，導(dǎo)致矛盾。q證：證：n=1時(shí)，因時(shí)，因C1S，顯然，顯然( C1 ) = 1。 q設(shè)對(duì)任意設(shè)對(duì)任意k n，( Ck ) = 1，考慮，考慮Cn 。若。若CnS，則應(yīng)有，則應(yīng)有q ( Cn ) = 1；若；若Cn 為為Ci , Cj 的消解結(jié)果，而的消解結(jié)果，而i,j n 。q據(jù)歸納假設(shè)，據(jù)歸納假設(shè)，q有有 ( Ci ) = 1，( Cj ) = 1，從而根據(jù)定理，從而根據(jù)定理1可得可得

7、( Cn ) = 1。 92.4 可滿足性問(wèn)題與消解法q闡明：闡明：q如果子句集如果子句集S是不可滿足的，那么必定存在由是不可滿足的，那么必定存在由S導(dǎo)出空子句的一個(gè)否證。導(dǎo)出空子句的一個(gè)否證。q我們可以利用消解原理作出我們可以利用消解原理作出S的否證，以證明的否證，以證明S的不可滿足性。的不可滿足性。102.4 可滿足性問(wèn)題與消解法q例例 設(shè)子句集設(shè)子句集S由以下四個(gè)子句組成：由以下四個(gè)子句組成：q （1）pqq （2pqq （3pqq （4）pqq證明證明S是不可滿足的。是不可滿足的。q可如下作出可如下作出S的否證：的否證：q （5q 由由1），（），（2消解得消解得q （6）q 由由3）

8、，（），（4消解得消解得q （7 由由5），（），（6消解得消解得112.4 可滿足性問(wèn)題與消解法q 例：例： 求證求證 (pq)(pr)(pqr) 永真永真 。q 證證 S為上式的否定的子句集，為上式的否定的子句集，S由以下子句組成：由以下子句組成：q （1）pqq （2）prq （3pq （4）qrq 作出作出S的否證：的否證：q （5q 由由1），（），（3消解得消解得q （6r 由由2），（），（3消解得消解得q （7）r 由由4），（），（5消解得消解得q （8 由由6），（），（7消解得消解得q 因此因此 (pq)(pr)(pqr) 為永真式。為永真式。122.4 可滿足性問(wèn)題與消解法q闡明：闡明：q一般命題公式都可化成等值的合取范式一般命題公式都可化成等值的合取范式q合取范式是不可滿足的當(dāng)且僅當(dāng)它有否證合取范式是不可滿足的當(dāng)且僅當(dāng)它有否證q用消解原理進(jìn)行推理是完全可