东南大学离散数学课件

1、12.4 可满足性问题与消解法可满足性问题与消解法q可满足性问题：可满足性问题：v用于证明用于证明A是否永真是否永真v用于验证逻辑蕴涵用于验证逻辑蕴涵 A1 Ak B 永真永真 当且仅当当且仅当 A1 Ak B 永假永假v真值表真值表v主析取范式主析取范式v主合取范式主合取范式u缺点：计算量大缺点：计算量大22.4 可满足性问题与消解法可满足性问题与消解法q无论是命题演算还是谓词演算，自然推理系统无论是命题演算还是谓词演算，自然推理系统是比较便于使用的，但对于计算机实现来说，是比较便于使用的，但对于计算机实现来说，仍然过于复杂。仍然过于复杂。 q消解法消解法32.4 可满足性问题与消解法可满足

2、性问题与消解法q 分离规则分离规则 可改为可改为 q 说明：说明：v该规则要求该规则要求“消去两个互补文字消去两个互补文字”。v“操作操作”特色特色v对第二种形式作如下的推广：对第二种形式作如下的推广： qqpp,qqpp,（1）mnmnrrqqrrpqqp.,.111142.4 可满足性问题与消解法可满足性问题与消解法q设设C1，C2为两个简单析取式，称为为两个简单析取式，称为子句子句，L1，L2是分别属于是分别属于C1，C2的互补文字对，用的互补文字对，用C-L表示从表示从子句子句C中删除文字中删除文字L后所得的子句，那么消解原理后所得的子句，那么消解原理可表示为：可表示为： 其中C1,C

3、2称为消解母式消解母式，L1，L2称为消解基消解基，而(C1-L1)(C2-L2)称为消解结果消解结果。)22() 11(2, 1LCLCCC52.4 可满足性问题与消解法可满足性问题与消解法q例：设例：设C1为为RPQ，C2为为PQv以以P，P为消解基的消解结果是为消解基的消解结果是 RQQv以以Q，Q为消解基的消解结果是为消解基的消解结果是RPPq特别地，当特别地，当C1，C2都是单文字子句，且互补时，都是单文字子句，且互补时，C1，C2的消解结果不含有任何文字，这时我们称的消解结果不含有任何文字，这时我们称其消解结果是其消解结果是“空子句空子句”（nil），常用符号），常用符号 表表示之

4、示之, 空子句空子句是永远无法被满足的。是永远无法被满足的。62.4 可满足性问题与消解法可满足性问题与消解法q定理定理1： 设设C是是C1，C2的消解结果，那么的消解结果，那么C是是C1和和C2的逻辑结果。的逻辑结果。q说明说明v消解原理作为推理规则是适当的。消解原理作为推理规则是适当的。v作为特别情况，作为特别情况，p与与p的消解结果是的消解结果是 ， 实质上实质上是是pp的另一种表示形式的另一种表示形式,它们都是不可满足的它们都是不可满足的。v给定一个合取范式给定一个合取范式S，S的所有简单析取式称为的所有简单析取式称为S的子句集。重复使用消解规则，可以的到一个子的子句集。重复使用消解规

5、则，可以的到一个子句序列。句序列。72.4 可满足性问题与消解法可满足性问题与消解法q定义定义： 设设S为一子句集，称为一子句集，称C是是S的消解结果，如的消解结果，如果存在一个子句序列果存在一个子句序列C1，C2 ，,Cn（= C），），使使Ci(i = 1,2, ,n) v或者是或者是S中子句，中子句，v或者是或者是Ck，Cj (k,j i) 的消解结果。的消解结果。v该序列称为是由该序列称为是由S导出的导出的C的消解序列。的消解序列。v当当是是S的消解结果时，称该序列为的消解结果时，称该序列为S的一个的一个否证否证（refutations）。）。82.4 可满足性问题与消解法可满足性问题

6、与消解法q定理定理2：如果子句集：如果子句集S有一个否证，那么有一个否证，那么S是不可是不可满足的。满足的。分析分析：设设C1，C2 ，,Cn（= ）是）是S的一个否证。若的一个否证。若S可满可满足，即有某个赋值足，即有某个赋值 使使S中所有子句为真，那么可对中所有子句为真，那么可对n归纳归纳证明，证明， 使使C1，C2 ，,Cn为真，从而为真，从而 ( Cn ) = () = 1，导致矛盾。导致矛盾。证：证：n=1时，因时，因C1 S，显然，显然 ( C1 ) = 1。 设对任意设对任意k n， ( Ck ) = 1，考虑，考虑Cn 。若。若Cn S，则应有，则应有 ( Cn ) = 1；若

7、；若Cn 为为Ci , Cj 的消解结果，而的消解结果，而i,j n 。据归纳假设，据归纳假设，有有 ( Ci ) = 1， ( Cj ) = 1，从而根据定理，从而根据定理1可得可得 ( Cn ) = 1。 92.4 可满足性问题与消解法可满足性问题与消解法q说明：说明：v如果子句集如果子句集S是不可满足的，那么必定存在由是不可满足的，那么必定存在由S导导出空子句的一个否证。出空子句的一个否证。v我们可以利用消解原理作出我们可以利用消解原理作出S的否证，以证明的否证，以证明S的的不可满足性。不可满足性。102.4 可满足性问题与消解法可满足性问题与消解法q例例 设子句集设子句集S由以下四个子

8、句组成：由以下四个子句组成： （1）pq （2）pq （3）pq （4）pq证明证明S是不可满足的。是不可满足的。q可如下作出可如下作出S的否证：的否证： （5）q 由（由（1），（），（2）消解得）消解得 （6）q 由（由（3），（），（4）消解得）消解得 （7） 由（由（5），（），（6）消解得）消解得112.4 可满足性问题与消解法可满足性问题与消解法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 可满足性问题与消解法可满足性问题与消解法q说明：说明：v一般命题公式都可化成等值的合取范式一般命题公式都可化成等值的合取范式v合取范式是不可满足的当且仅当它有否证合取范式是不可满足的当且仅当它有否证v用消解原理进