离散-2.4

3
2.4 消解法
C1 ∧ C2和Res(C1,C2)不等值 不等值 ∨¬r 例：C1=p∨q∨r, C2=p∨¬ ∨ ∨ ∨¬
Res(C1,C2) = p∨q ∨ v=FTT满足 满足Res(C1,C2) 但不满足 1 ∧ C2 但不满足C 满足
4
2.4 消解法
消解推导： 消解推导：S=C1 ∧… ∧ Cn和C
lc=¬p，如果 =p ¬ ，如果l lc=p，如果 = ¬p ，如果l
消解式： 消解式：C1= C′1 ∨ l, C2= C′2 ∨ lc Res(C1,C2)= C′1 ∨ C′2 定理： 定理：C1 ∧ C2 ⊨ Res(C1,C2)
消解式是原公式的逻辑推论 讨论！ 讨论！
2
2.4 消解法
定理： 定理： C1 ∧ C2和Res(C1,C2)可满足性相同 可满足性相同 证明： 证明：C1= C′1 ∨ l, C2= C′2 ∨ lc 如果C 可满足，则存在v， 如果 1 ∧ C2可满足，则存在 ，v(Ci)=T 假设v(l)=T，则v(C′2)=T。 假设 ， 。 如果Res(C1,C2)可满足，则存在 可满足， 如果 可满足 则存在v v(C′1 ∨ C′2)=T 存在l’在 使得v(l’)=T, v可以扩展为 存在 在C′1使得 可以扩展为 v(p)=F 如果p=l 如果 v(p)=T 如果 如果p=lc v对C1 ∧ C2赋值为 赋值为T 对
9
2.4 消解法
消解算法（分层饱和法） 消解算法（分层饱和法） 输入：合式公式A 输入：合式公式 输出： 可满足)， 不可满足) 输出：yes (A可满足 ，no (A不可满足 可满足 不可满足
1. 求A的合取范式 的合取范式S. 的合取范式 2. 令i=1, S(0)=S. 3. 若S(i)包含空子句，则S不可满足，算法终止 包含空子句， 不可满足， 不可满足 算法终止. 4. i=i+1. 5. 构造 (i)={Res(C1,C2) | C1∈(S(0) ⋃… ⋃ S(i-1))且C2 ∈ S(i-1)}. 构造S 且 6. 若S(i) ⊂ S(0) ⋃ … ⋃ S(i-1)则S是可满足的，算法终止 是可满足的， 是可满足的 算法终止. 7. 转3
2.4 消解法
可满足性问题： 可满足性问题：
用于证明A是否永真 用于证明 是否永真 用验证逻辑蕴涵
• A1∧…∧Ak → B 永真 当且仅当 A1∧…∧Ak ∧¬ B 永假 ∧ ∧
解决方法
真值表 主析取范式 主合取范式 缺点： 缺点：计算量大
引入消解法！ 引入消解法！
1
2.4 消解法
文字l的补： 文字 的补： 的补
7
2.4 消解法
消解完全性：如果合取范式 是不可满足 消解完全性：如果合取范式S是不可满足，则S 是不可满足， 有否证 证明： 中所含命题个数k归纳证明 证明：对S中所含命题个数 归纳证明 中所含命题个数 中有p, 第一步骤 k=1: S中有 ¬p 中有 假设k<n时定理成立，证明 时定理成立， 第二步骤 假设 时定理成立 证明k=n时定 时定 理成立 1. 对S ∧ p应用引理 ，得到等满足性的 应用引理1，得到等满足性的S’ 应用引理 2. 对S ∧ ¬p应用引理 ，得到等满足性的 应用引理1，得到等满足性的S’’ 应用引理 由假设，存在S’的否证 的否证C 由假设，存在 的否证 1,…,Ci，S’’的否证 的否证 D1,…,Dj
6
2.4 消解法
引理1 如果合取范式S含有文字 引理1：如果合取范式 含有文字 ，S’为 含有文字l， 为
S先删除包含 的简单析取式 先删除包含l的简单析取式 先删除包含 再删除剩下的简单析取式中l 再删除剩下的简单析取式中 c 则S和S’可满足性相同 和 可满足性相同
证明： 如果 为满足 的赋值，S含有文字 ， 为满足S的赋值 含有文字l， 证明： 如果v为满足 的赋值， 含有文字 v(l)=T，对任意 中C’，必有 ，对任意S’中 ，必有v(S’)=T。 。 如果v为满足 的赋值，则可以扩展为满足S的 为满足S’的赋值 如果 为满足 的赋值，则可以扩展为满足 的 赋值（验证）！ 赋值（验证）！
5
2.4 消解法
消解可靠性：如果合取范式 有否证 消解可靠性：如果合取范式S有否证，则S是不 有否证， 是不 可满足 证明：每次使用消解，都保持可满足性。 证明：每次使用消解，都保持可满足性。如果 消解结果不可满足， 必不可满足。 消解结果不可满足，则S必不可满足。 必不可满足 消解完全性：如果合取范式S是不可满足 是不可满足， 消解完全性：如果合取范式 是不可满足，则S 有否证
8
2.4 消解法
证明（继续）： 证明（继续）： 1. 对S ∧ p应用引理 ，得到等满足性的 应用引理1，得到等满足性的S’ 应用引理 2. 对S ∧ ¬p应用引理 ，得到等满足性的 应用引理1，得到等满足性的S’’ 应用引理 由假设，存在S’的否证 的否证C 由假设，存在 的否证 1,…,Ci，S’’的否证 的否证 D1,…,Dj 情况1： 都在S中 情况 ：Ct (i≥t≥1)或Ds (j≥t≥1)都在 中， C1,…,Ci ≥ ≥ 或 ≥ ≥ 都在 或D1,…,Dj为S的否证 的否证 情况2： 不满足情况1条件 情况 ： Ct (或Ds)不满足情况 条件，则扩展 t (或 或 不满足情况 条件，则扩展C 或 Ds)得到 t= Ct ∨ ¬p (或D′s = Ds ∨ p ) ，则C′t ( 得到C′ 得到 或 属于S 或D′s )属于 ，且 属于 C′i= ¬p， D′j=p，消解得到空子句□ 空子句□ ， ，消解得到空子句
符号： 符号：{C1,…,Cn} ⊢ C 存在公式序列A 对每个i(i=1,…,k), 存在公式序列 1, A2,…,Ak，对每个
• Ai是某个 j或者 是某个C • Ai是有序列中前面的公式应用消解得到 • Ak=C
是由S到 的推导 称A1,…,Ak是由 到C的推导 如果C 为空子句□ 则称此序列是S的一个否证 如果 为空子句□，则称此序列是 的一个否证
12
¬p ∨ q ¬q ∨ p ¬q ∨ ¬p q
10
2.4 消解法
例1：A=(¬p∨q) ∧ (p∨q) ∧ (¬q) ： ¬ ∨ ∨ ¬
S(0) = {¬p∨q, p∨q, ¬q} ¬ ∨ ∨ S(1)={q, ¬p, p} 算法终止
11
2.4 消解法
∨¬q, ∨¬q} 例2：S={¬p∨q, p∨q, p∨¬ ¬p∨¬ ： ¬ ∨ ∨ ∨¬ ∨¬ p∨q q p ¬q □