2 智能系统学报 第9卷 基于归结的方法[s6)、基于表推演的方法、基于 近子句集簇，记为(，T), 自然演绎的方法、基于公理系统的方法、基于相继式 (x V,= 演算的方法和基于扩展规则的方法[)是儿类主要 r=0,={区-， =1 其他 的定理证明方法。其中基于归结的定理证明方法一 x为M中的任意变量。 直是最重要也是最基本的方法，其基本思想是通过 定义4(#SAT问题)给定一个命题公式∑， 推出空子句判定给定子句集的不可满足性。相反于 SAT问题就是计算∑的可满足赋值（模型）个数。 归结方法，基于扩展规则的方法的基本思想是将定 定义5（加权模型计数问题）)给定子句集 理证明沿着归结的逆向进行，通过推出所有极大项 ∑，∑中的每个文字l的权记作()，每个模型w的 组成的集合来判定子句集的可满足性。该方法不需 权为 要将所有极大项都扩展出来，而是巧妙地利用容斥 W(w)=Πo() 原理直接计算扩展出的极大项的个数，降低了其空 =1 间复杂性，对于互补因子较高的SAT问题具有独特 加权模型计数问题是计算满足Σ的所有模型的权 的求解优势，被国际著名的人工智能专家、DP过程 之和。 的提出者Davis教授称为归结方法的补方法[8。 SAT问题可以看作是加权模型计数问题的特 基于扩展规则的定理证明方法于2003年由Lin 例，其中每个文字的权值为0.5。 等[]提出，发表在国际重要杂志《Joumal of Automa- 隐蔽集(backdoor set)和骨架集(backbone set) ted Reasoning》上，该方法一经提出就受到了国内外 是SAT问题的重要结构，与问题求解难度有着密切 学者的广泛关注，出现了大量研究成果。本文对扩 的关系[2]。 展规则方法自提出以来10年的发展情况进行总结， 定义6（隐蔽集）[]给定一个命题公式∑， 旨在让对该方向感兴趣的学者有一个较为全面的 B二Var()非空，如果B中变量的任意（存在一 了解。 个)真值指派t使得简化公式[t]在多项式时间内 可解，那么B为Σ的强（弱）隐蔽集：如果简化公式 1 相关概念 -B能在多项式时间内求解，那么B为Σ的删除隐 在定理证明的几类求解方法中，扩展规则方法 蔽集。当基本类是封闭的，删除隐蔽集等价于强隐 以其独特的特点和求解优势引起了研究者的广泛关 蔽集。 注，这里介绍所涉及的相关概念。首先对文中符号 定义7（骨架集）【4给定一个命题公式Σ， 进行约定：用∑表示合取范式(conjunctive normal B CVar()非空，如果在所有模型中，B中变量的 fom,CNF),也看作子句集，有时也称为公式，用C 赋值都相同，那么B为Σ的骨架集。 表示单个的子句，可以理解为文字的集合：用小写英 定义8（扩展规则）[]给定一个子句C和一 文字母表示布尔变量（简称变量），也称作原子，用 个变量的集合M,D={CVa,CV-a I a∈M并且 |I表示∑中子句的个数，Var()表示出现在∑中 a和a都不在C中出现}，那么把从C到D中元素 的变量，IC1表示子句中的变量个数，Mod()表示 的推导过程叫做扩展规则，D中的元素叫做应用扩 所有模型组成的集合。 展规则的结果。 定义1(SAT问题)给定一个命题公式∑，SAT 定义9（极大项）[)设C为变量集合M上的 问题就是判断是否存在一个真值赋值使得公式的值 一个非重言式子句，且IM=m,如果1C1=m,那么C 为真。若存在，则称Σ是可满足的，否则为不可满 为M上的极大项。 足的。 定义10（互补因子）[)给定子句集Σ，11= 定义2（碰集）给定集合簇T,如果 n,互补因子C是含互补对的子句对个数与所有子 H CUseTS,且对于每一个S∈T,都有 句对个数的比值，即C=S/C2,其中S表示含互补 H∩S≠☑，那么称H为T的一个碰集。如果H 对的子句对个数。 是满足上述性质的极小集合，则称H为极小碰集。 定义3（相近SAT问题）[1o)对于变量集M上 2命题逻辑中的扩展规则求解方法 的k(k>I)个子句集，三2，…，三，令Σ=三n 扩展规则方法始于命题逻辑，本节分别讨论其 2∩…∩，若对于1≤i≤k有1-1≤1， 在SAT问题、相近SAT问题和#SAT问题中的研究 则称三，2，…，三相近，由它们构成的集合称为相 进展。基于归结的方法［５⁃６］ 、基于表推演的方法、基于 自然演绎的方法、基于公理系统的方法、基于相继式 演算的方法和基于扩展规则的方法［７］ 是几类主要 的定理证明方法。 其中基于归结的定理证明方法一 直是最重要也是最基本的方法，其基本思想是通过 推出空子句判定给定子句集的不可满足性。 相反于 归结方法，基于扩展规则的方法的基本思想是将定 理证明沿着归结的逆向进行，通过推出所有极大项 组成的集合来判定子句集的可满足性。 该方法不需 要将所有极大项都扩展出来，而是巧妙地利用容斥 原理直接计算扩展出的极大项的个数，降低了其空 间复杂性，对于互补因子较高的 ＳＡＴ 问题具有独特 的求解优势，被国际著名的人工智能专家、ＤＰ 过程 的提出者 Ｄａｖｉｓ 教授称为归结方法的补方法［８⁃９］ 。 基于扩展规则的定理证明方法于 ２００３ 年由 Ｌｉｎ 等［７］提出，发表在国际重要杂志《 Ｊｏｕｍａｌ ｏｆ Ａｕｔｏｍａ⁃ ｔｅｄ Ｒｅａｓｏｎｉｎｇ》上，该方法一经提出就受到了国内外 学者的广泛关注，出现了大量研究成果。 本文对扩 展规则方法自提出以来 １０ 年的发展情况进行总结， 旨在让对该方向感兴趣的学者有一个较为全面的 了解。 １ 相关概念 在定理证明的几类求解方法中，扩展规则方法 以其独特的特点和求解优势引起了研究者的广泛关 注，这里介绍所涉及的相关概念。 首先对文中符号 进行约定：用 Σ 表示合取范式（ ｃｏｎｊｕｎｃｔｉｖｅ ｎｏｒｍａｌ ｆｏｒｍ， ＣＮＦ），也看作子句集，有时也称为公式，用 Ｃ 表示单个的子句，可以理解为文字的集合；用小写英 文字母表示布尔变量（简称变量），也称作原子，用 ｜ Σ ｜表示 Σ 中子句的个数，Ｖａｒ（Σ）表示出现在 Σ 中 的变量， ｜ Ｃ ｜表示子句中的变量个数，Ｍｏｄ（Σ）表示 Σ 所有模型组成的集合。 定义 １（ＳＡＴ 问题） 给定一个命题公式 Σ，ＳＡＴ 问题就是判断是否存在一个真值赋值使得公式的值 为真。 若存在，则称 Σ 是可满足的，否则为不可满 足的。 定 义 ２ （ 碰 集 ） 给 定 集 合 簇 Ｔ， 如 果 Ｈ ⊆∪Ｓ∈Ｔ Ｓ ， 且 对 于 每 一 个 Ｓ ∈ Ｔ ， 都 有 Ｈ ∩ Ｓ ≠ ∅， 那么称 Ｈ 为 Ｔ 的一个碰集。 如果 Ｈ 是满足上述性质的极小集合，则称 Ｈ 为极小碰集。 定义 ３（相近 ＳＡＴ 问题） ［１０］ 对于变量集 Ｍ 上 的 ｋ （ ｋ ＞ １） 个子句集 Σ１ ，Σ２ ，…，Σｋ，令 Σ ＝ Σ１ ∩ Σ２ ∩… ∩ Σｋ， 若对于 ∀１ ≤ ｉ ≤ ｋ 有 ｜ Σｉ － Σ ｜ ≤１， 则称 Σ１ ，Σ２ ，…，Σｋ 相近，由它们构成的集合称为相 近子句集簇，记为 （Σ，Γ） ， Γ ＝∪ ｍ ｉ ＝ １ Σｉ ′，Σｉ ′ ＝ ｛ｘ ∨ Øｘ｝，Σｉ ＝ Σ Σｉ { － Σ， 其他 ｘ 为 Ｍ 中的任意变量。 定义 ４ （ ＃ ＳＡＴ 问题） 给定一个命题公式 Σ， ＃ＳＡＴ问题就是计算 Σ 的可满足赋值（模型）个数。 定义 ５（加权模型计数问题） ［１１］ 给定子句集 Σ，Σ 中的每个文字 ｌ 的权记作 ｗ（ｌ），每个模型 ω 的 权为 Ｗ（ω） ＝ ∏ω｜ ＝ ｌ ｗ（ｌ） 加权模型计数问题是计算满足 Σ 的所有模型的权 之和。 ＃ＳＡＴ 问题可以看作是加权模型计数问题的特 例，其中每个文字的权值为 ０．５。 隐蔽集（ｂａｃｋｄｏｏｒ ｓｅｔ）和骨架集（ ｂａｃｋｂｏｎｅ ｓｅｔ） 是 ＳＡＴ 问题的重要结构，与问题求解难度有着密切 的关系［１２］ 。 定义 ６ （隐蔽集） ［１３］ 给定一个命题公式 Σ， Ｂ ⊆Ｖａｒ（Σ） 非空，如果 Ｂ 中变量的任意（ 存在一 个）真值指派 ｔ 使得简化公式 Σ［ｔ］在多项式时间内 可解，那么 Ｂ 为 Σ 的强（弱）隐蔽集；如果简化公式 Σ－Ｂ 能在多项式时间内求解，那么 Ｂ 为 Σ 的删除隐 蔽集。 当基本类是封闭的，删除隐蔽集等价于强隐 蔽集。 定义 ７（骨架集） ［１４］ 给定一个命题公式 Σ， Ｂ ⊆Ｖａｒ（Σ） 非空，如果在所有模型中，Ｂ 中变量的 赋值都相同，那么 Ｂ 为 Σ 的骨架集。 定义 ８（扩展规则） ［７］ 给定一个子句 Ｃ 和一 个变量的集合 Ｍ，Ｄ ＝ ｛Ｃ∨ａ， Ｃ∨Øａ ｜ ａ∈Ｍ 并且 ａ 和Øａ 都不在 Ｃ 中出现｝，那么把从 Ｃ 到 Ｄ 中元素 的推导过程叫做扩展规则，Ｄ 中的元素叫做应用扩 展规则的结果。 定义 ９（极大项） ［７］ 设 Ｃ 为变量集合 Ｍ 上的 一个非重言式子句，且｜ Ｍ｜ ＝ｍ，如果｜ Ｃ ｜ ＝ ｍ，那么 Ｃ 为 Ｍ 上的极大项。 定义 １０（互补因子） ［７］ 给定子句集 Σ， ｜ Σ ｜ ＝ ｎ，互补因子 ＣＦ 是含互补对的子句对个数与所有子 句对个数的比值，即 ＣＦ ＝ Ｓ ／ Ｃ ２ ｎ ，其中 Ｓ 表示含互补 对的子句对个数。 ２ 命题逻辑中的扩展规则求解方法 扩展规则方法始于命题逻辑，本节分别讨论其 在 ＳＡＴ 问题、相近 ＳＡＴ 问题和＃ＳＡＴ 问题中的研究 进展。 ·２· 智 能 系 统 学 报 第 ９ 卷