《东南大学离散数学课件.ppt》由会员分享,可在线阅读,更多相关《东南大学离散数学课件.ppt(12页珍藏版)》请在三一文库上搜索。
1、2.4 可满足性问题与消解法,可满足性问题: 用于证明A是否永真 用于验证逻辑蕴涵 A1Ak B 永真 当且仅当 A1Ak B 永假 解决方法 真值表 主析取范式 主合取范式 缺点:计算量大,2.4 可满足性问题与消解法,无论是命题演算还是谓词演算,自然推理系统是比较便于使用的,但对于计算机实现来说,仍然过于复杂。 消解法,2.4 可满足性问题与消解法,分离规则 可改为 说明: 该规则要求“消去两个互补文字”。 “操作”特色 对第二种形式作如下的推广:,(1),2.4 可满足性问题与消解法,设C1,C2为两个简单析取式,称为子句,L1,L2是分别属于C1,C2的互补文字对,用C-L表示从子句C
2、中删除文字L后所得的子句,那么消解原理可表示为: 其中C1,C2称为消解母式,L1,L2称为消解基,而(C1-L1)(C2-L2)称为消解结果。,2.4 可满足性问题与消解法,例:设C1为RPQ,C2为PQ 以P,P为消解基的消解结果是 RQQ 以Q,Q为消解基的消解结果是RPP 特别地,当C1,C2都是单文字子句,且互补时,C1,C2的消解结果不含有任何文字,这时我们称其消解结果是“空子句”(nil),常用符号 表示之, 空子句是永远无法被满足的。,2.4 可满足性问题与消解法,定理1: 设C是C1,C2的消解结果,那么C是C1和C2的逻辑结果。 说明 消解原理作为推理规则是适当的。 作为特
3、别情况,p与p的消解结果是 , 实质上是pp的另一种表示形式,它们都是不可满足的。 给定一个合取范式S,S的所有简单析取式称为S的子句集。重复使用消解规则,可以的到一个子句序列。,2.4 可满足性问题与消解法,定义: 设S为一子句集,称C是S的消解结果,如果存在一个子句序列C1,C2 ,,Cn(= C),使Ci(i = 1,2, ,n) 或者是S中子句, 或者是Ck,Cj (k,j i) 的消解结果。 该序列称为是由S导出的C的消解序列。 当是S的消解结果时,称该序列为S的一个否证 (refutations)。,2.4 可满足性问题与消解法,定理2:如果子句集S有一个否证,那么S是不可满足的。
4、 分析:设C1,C2 ,,Cn(= )是S的一个否证。若S可满足,即有某个赋值使S中所有子句为真,那么可对n归纳证明,使C1,C2 ,,Cn为真,从而( Cn ) = () = 1,导致矛盾。 证:n=1时,因C1S,显然( C1 ) = 1。 设对任意k n,( Ck ) = 1,考虑Cn 。若CnS,则应有 ( Cn ) = 1;若Cn 为Ci , Cj 的消解结果,而i,j n 。 据归纳假设, 有 ( Ci ) = 1,( Cj ) = 1,从而根据定理1可得 ( Cn ) = 1。,2.4 可满足性问题与消解法,说明: 如果子句集S是不可满足的,那么必定存在由S导出空子句的一个否证。
5、 我们可以利用消解原理作出S的否证,以证明S的不可满足性。,2.4 可满足性问题与消解法,例 设子句集S由以下四个子句组成: (1)pq (2)pq (3)pq (4)pq 证明S是不可满足的。 可如下作出S的否证: (5)q 由(1),(2)消解得 (6)q 由(3),(4)消解得 (7) 由(5),(6)消解得,2.4 可满足性问题与消解法,例: 求证 (pq)(pr)(pqr) 永真 。 证 S为上式的否定的子句集,S由以下子句组成: (1)pq (2)pr (3)p (4)qr 作出S的否证: (5)q 由(1),(3)消解得 (6)r 由(2),(3)消解得 (7)r 由(4),(5)消解得 (8) 由(6),(7)消解得 因此 (pq)(pr)(pqr) 为永真式。,2.4 可满足性问题与消解法,说明: 一般命题公式都可化成等值的合取范式 合取范式是不可满足的当且仅当它有否证 用消解原理进行推理是完全可以用计算机来实现的。当然,如果让机器盲目地进行消解,会产生许多不必要的消解及大量未必有用的中间结果,因而效率是不高的 。,
链接地址:https://www.31doc.com/p-2203285.html