東南大學(xué)離散數(shù)學(xué)課件

1、12.4 可滿足性問(wèn)題與消解法可滿足性問(wèn)題與消解法q可滿足性問(wèn)題：可滿足性問(wèn)題：v用于證明用于證明A是否永真是否永真v用于驗(yàn)證邏輯蘊(yùn)涵用于驗(yàn)證邏輯蘊(yùn)涵 A1 Ak B 永真永真 當(dāng)且僅當(dāng)當(dāng)且僅當(dāng) A1 Ak B 永假永假v真值表真值表v主析取范式主析取范式v主合取范式主合取范式u缺點(diǎn)：計(jì)算量大缺點(diǎn)：計(jì)算量大22.4 可滿足性問(wèn)題與消解法可滿足性問(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)題與消解法可滿足

2、性問(wèn)題與消解法q 分離規(guī)則分離規(guī)則 可改為可改為 q 說(shuō)明：說(shuō)明：v該規(guī)則要求該規(guī)則要求“消去兩個(gè)互補(bǔ)文字消去兩個(gè)互補(bǔ)文字”。v“操作操作”特色特色v對(duì)第二種形式作如下的推廣：對(duì)第二種形式作如下的推廣： qqpp,qqpp,（1）mnmnrrqqrrpqqp.,.111142.4 可滿足性問(wèn)題與消解法可滿足性問(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后所得的子句，那么消解原理后所得的子句，那么消解原理可表示為：可表示為： 其中C1,C

3、2稱為消解母式消解母式，L1，L2稱為消解基消解基，而(C1-L1)(C2-L2)稱為消解結(jié)果消解結(jié)果。)22() 11(2, 1LCLCCC52.4 可滿足性問(wèn)題與消解法可滿足性問(wèn)題與消解法q例：設(shè)例：設(shè)C1為為RPQ，C2為為PQv以以P，P為消解基的消解結(jié)果是為消解基的消解結(jié)果是 RQQv以以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) 表表示之

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

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

6、與消解法q定理定理2：如果子句集：如果子句集S有一個(gè)否證，那么有一個(gè)否證，那么S是不可是不可滿足的。滿足的。分析分析：設(shè)設(shè)C1，C2 ，,Cn（= ）是）是S的一個(gè)否證。若的一個(gè)否證。若S可滿可滿足，即有某個(gè)賦值足，即有某個(gè)賦值 使使S中所有子句為真，那么可對(duì)中所有子句為真，那么可對(duì)n歸納歸納證明，證明， 使使C1，C2 ，,Cn為真，從而為真，從而 ( Cn ) = () = 1，導(dǎo)致矛盾。導(dǎo)致矛盾。證：證：n=1時(shí)，因時(shí)，因C1 S，顯然，顯然 ( C1 ) = 1。 設(shè)對(duì)任意設(shè)對(duì)任意k n， ( Ck ) = 1，考慮，考慮Cn 。若。若Cn S，則應(yīng)有，則應(yīng)有 ( Cn ) = 1；若

7、；若Cn 為為Ci , Cj 的消解結(jié)果，而的消解結(jié)果，而i,j n 。據(jù)歸納假設(shè)，據(jù)歸納假設(shè)，有有 ( Ci ) = 1， ( Cj ) = 1，從而根據(jù)定理，從而根據(jù)定理1可得可得 ( Cn ) = 1。 92.4 可滿足性問(wèn)題與消解法可滿足性問(wèn)題與消解法q說(shuō)明：說(shuō)明：v如果子句集如果子句集S是不可滿足的，那么必定存在由是不可滿足的，那么必定存在由S導(dǎo)導(dǎo)出空子句的一個(gè)否證。出空子句的一個(gè)否證。v我們可以利用消解原理作出我們可以利用消解原理作出S的否證，以證明的否證，以證明S的的不可滿足性。不可滿足性。102.4 可滿足性問(wèn)題與消解法可滿足性問(wèn)題與消解法q例例 設(shè)子句集設(shè)子句集S由以下四個(gè)子

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