【学术论文】扩展规则方法研究综述

第9卷第1期 智能系统学报 Vol.9 No.1 2014年2月 CAAI Transactions on Intelligent Systems Feb.2014 D0:10.3969/j.issn.1673-4785.201308004 网络出版地址：http:/www.cmki.net/kcms/doi/10.3969/j.issn.1673-4785.201308004.html 扩展规则方法研究综述 王金艳，谷文祥3，章少华，般明浩3 (1.广西师范大学计算机科学与信息工程学院，广西柱林541004：2.长春建筑学院基础教学部，吉林长春130607： 3.东北师范大学计算机科学与信息技术学院，吉林长春130117) 摘要：归结方法是自动推理的重要方法之一，而扩展规则是与归结对称的方法，近年来引起了研究者的广泛关注。 从扩展规则的相关概念、在命题逻辑中的发展以及在一阶逻辑、描述逻辑、模态逻辑、可能性逻辑和多值逻辑中的应 用3个方面论述分析了扩展规则10年来的研究现状，重点阐述扩展规则用于求解SAT、相近SAT和#SAT问题各种 算法的优缺点，最后指出相关的研究热点与发展趋势。 关键词：自动推理；归结方法：扩展规则；SAT;sAT 中图分类号：TP181文献标志码：A文章编号：1673-4785(2014)01-0001-11 中文引用格式：王金艳，谷文祥，覃少华，等.扩展规则方法研究综述[J].智能系统学报，2014,9(1)：1-11 英文引用格式：WANG Jinyan,GU Wenxiang,QIN Shaohua,etal.Extension rule:a survey[J】.CAAI Transactions on Intelligent Systems,2014,9(1):1-11. Extension rule:a survey WANG Jinyan',GU Wenxiang23,QIN Shaohua',YIN Minghao (1.School of Computer Science and Information Technology,Guangxi Normal University,Guilin 541004,China;2.Department of Basic Subjects Teaching,Changchun Architecture Civil Engineering College,Changchun 130607,China;3.School of Computer Sci- ence and Information Technology,Northeast Normal University,Changchun 130117,China) Abstract:The method based on the resolution principle has always been one of the important methods for automated reasoning.The theorem proving method using the extension rule is complementary to the method based on the reso- lution principle.In recent years,the method has received wide attention and has achieved great progress.This pa- per surveys the development of the theorem proving using the extension rule for ten years from three aspects:the re- lated concepts of the extension rule,the development of the propositional logic,and the applications for first-order logic,description logic,modal logic,possibility logic and multivalue logic,in which the merits and demerits of these algorithms for solving SAT,analogous SAT and #SAT using the extension rule are mainly analyzed.Finally, the related research hotspots and developing trends are pointed out. Keywords:automated reasoning;resolution principle;extension rule;SAT;#SAT 作为数理逻辑中形式化推理的一个分支，自动证和硬件校验方面，Karlsruhe大学开发的KIv[)已 推理在人工智能发展初期就引起了研究者的广泛关 成功用于验证许多应用软件，包括图和树的表示等 注。定理证明是领域的研究热点，其发展深刻地影 实验室软件和用于铁路转弯控制等工业软件，一些 响着人工智能乃至计算机科学的其他研究方向，并 大公司如英特尔、摩托罗拉、AMD等都使用基于定 在计算机工程中有着广泛的应用山。如在软件验 理证明的硬件校验技术。在智能规划领域，把规划 问题编译成SAT(satisfiablity)问题并利用高效的 SAT求解器进行求解已成为一种主要方法。基于 收稿日期：2013-08-07.网络出版日期：2014-02-20 基金项目：国家自然科学基金资助项目(61070084,61272535,61163065， SAT的规划系统，在两年一度的国际规划器竞赛中 61370156,61165009):国家“97”计划资助项目(2012CB32640B): 屡获冠军，表现出优异的性能[)。Grastien等[将 广西自然科学基金资助项目(2013 GXNSFBA019263, 2012 GXNSFAA053219):广西高校科研项目(2013YB029): 基于模型的诊断问题转化成SAT问题，并且利用 “八桂学者”工程专项经费资助项目：广西师范大学博士启 动基金资助项目. SAT求解算法进行诊断。与传统的方法相比，基于 通信作者：罩少华.E-mail:shqin@gnu.cu.cm. SAT的诊断方法能解决更复杂的诊断问题

第 ９ 卷第 １ 期 智 能 系 统 学 报 Ｖｏｌ．９ №．１ ２０１４ 年 ２ 月 ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ Ｆｅｂ． ２０１４ ＤＯＩ：１０．３９６９ ／ ｊ．ｉｓｓｎ．１６７３⁃４７８５．２０１３０８００４ 网络出版地址：ｈｔｔｐ： ／ ／ ｗｗｗ．ｃｎｋｉ．ｎｅｔ ／ ｋｃｍｓ／ ｄｏｉ ／ １０．３９６９ ／ ｊ．ｉｓｓｎ．１６７３⁃４７８５．２０１３０８００４．ｈｔｍｌ 扩展规则方法研究综述 王金艳１ ，谷文祥２，３ ，覃少华１ ，殷明浩３ （１．广西师范大学 计算机科学与信息工程学院，广西 桂林 ５４１００４；２．长春建筑学院 基础教学部，吉林 长春 １３０６０７； ３． 东北师范大学 计算机科学与信息技术学院，吉林 长春 １３０１１７） 摘 要：归结方法是自动推理的重要方法之一，而扩展规则是与归结对称的方法，近年来引起了研究者的广泛关注。 从扩展规则的相关概念、在命题逻辑中的发展以及在一阶逻辑、描述逻辑、模态逻辑、可能性逻辑和多值逻辑中的应 用 ３ 个方面论述分析了扩展规则 １０ 年来的研究现状，重点阐述扩展规则用于求解 ＳＡＴ、相近 ＳＡＴ 和＃ＳＡＴ 问题各种 算法的优缺点，最后指出相关的研究热点与发展趋势。 关键词：自动推理；归结方法；扩展规则；ＳＡＴ； ＃ＳＡＴ 中图分类号：ＴＰ１８１ 文献标志码：Ａ 文章编号：１６７３⁃４７８５（２０１４）０１⁃０００１⁃１１ 中文引用格式：王金艳，谷文祥，覃少华，等．扩展规则方法研究综述［Ｊ］． 智能系统学报， ２０１４， ９（１）： １⁃１１． 英文引用格式：ＷＡＮＧ Ｊｉｎｙａｎ， ＧＵ Ｗｅｎｘｉａｎｇ， ＱＩＮ Ｓｈａｏｈｕａ， ｅｔ ａｌ． Ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ： ａ ｓｕｒｖｅｙ［Ｊ］． ＣＡＡＩ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓｔｅｍｓ， ２０１４， ９（１）： １⁃１１． Ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ： ａ ｓｕｒｖｅｙ ＷＡＮＧ Ｊｉｎｙａｎ １ ， ＧＵ Ｗｅｎｘｉａｎｇ ２，３ ， ＱＩＮ Ｓｈａｏｈｕａ １ ， ＹＩＮ Ｍｉｎｇｈａｏ ３ （１． Ｓｃｈｏｏｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｉｎｆｏｒｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏｇｙ， Ｇｕａｎｇｘｉ Ｎｏｒｍａｌ Ｕｎｉｖｅｒｓｉｔｙ， Ｇｕｉｌｉｎ ５４１００４， Ｃｈｉｎａ； ２． Ｄｅｐａｒｔｍｅｎｔ ｏｆ Ｂａｓｉｃ Ｓｕｂｊｅｃｔｓ Ｔｅａｃｈｉｎｇ， Ｃｈａｎｇｃｈｕｎ Ａｒｃｈｉｔｅｃｔｕｒｅ ＆ Ｃｉｖｉｌ Ｅｎｇｉｎｅｅｒｉｎｇ Ｃｏｌｌｅｇｅ， Ｃｈａｎｇｃｈｕｎ １３０６０７， Ｃｈｉｎａ； ３． Ｓｃｈｏｏｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉ⁃ ｅｎｃｅ ａｎｄ Ｉｎｆｏｒｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏｇｙ， Ｎｏｒｔｈｅａｓｔ Ｎｏｒｍａｌ Ｕｎｉｖｅｒｓｉｔｙ， Ｃｈａｎｇｃｈｕｎ １３０１１７， Ｃｈｉｎａ） Ａｂｓｔｒａｃｔ：Ｔｈｅ ｍｅｔｈｏｄ ｂａｓｅｄ ｏｎ ｔｈｅ ｒｅｓｏｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ ｈａｓ ａｌｗａｙｓ ｂｅｅｎ ｏｎｅ ｏｆ ｔｈｅ ｉｍｐｏｒｔａｎｔ ｍｅｔｈｏｄｓ ｆｏｒ ａｕｔｏｍａｔｅｄ ｒｅａｓｏｎｉｎｇ． Ｔｈｅ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ｍｅｔｈｏｄ ｕｓｉｎｇ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｉｓ ｃｏｍｐｌｅｍｅｎｔａｒｙ ｔｏ ｔｈｅ ｍｅｔｈｏｄ ｂａｓｅｄ ｏｎ ｔｈｅ ｒｅｓｏ⁃ ｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ． Ｉｎ ｒｅｃｅｎｔ ｙｅａｒｓ， ｔｈｅ ｍｅｔｈｏｄ ｈａｓ ｒｅｃｅｉｖｅｄ ｗｉｄｅ ａｔｔｅｎｔｉｏｎ ａｎｄ ｈａｓ ａｃｈｉｅｖｅｄ ｇｒｅａｔ ｐｒｏｇｒｅｓｓ． Ｔｈｉｓ ｐａ⁃ ｐｅｒ ｓｕｒｖｅｙｓ ｔｈｅ ｄｅｖｅｌｏｐｍｅｎｔ ｏｆ ｔｈｅ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ｕｓｉｎｇ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｆｏｒ ｔｅｎ ｙｅａｒｓ ｆｒｏｍ ｔｈｒｅｅ ａｓｐｅｃｔｓ： ｔｈｅ ｒｅ⁃ ｌａｔｅｄ ｃｏｎｃｅｐｔｓ ｏｆ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ， ｔｈｅ ｄｅｖｅｌｏｐｍｅｎｔ ｏｆ ｔｈｅ ｐｒｏｐｏｓｉｔｉｏｎａｌ ｌｏｇｉｃ， ａｎｄ ｔｈｅ ａｐｐｌｉｃａｔｉｏｎｓ ｆｏｒ ｆｉｒｓｔ⁃ｏｒｄｅｒ ｌｏｇｉｃ， ｄｅｓｃｒｉｐｔｉｏｎ ｌｏｇｉｃ， ｍｏｄａｌ ｌｏｇｉｃ， ｐｏｓｓｉｂｉｌｉｔｙ ｌｏｇｉｃ ａｎｄ ｍｕｌｔｉｖａｌｕｅ ｌｏｇｉｃ， ｉｎ ｗｈｉｃｈ ｔｈｅ ｍｅｒｉｔｓ ａｎｄ ｄｅｍｅｒｉｔｓ ｏｆ ｔｈｅｓｅ ａｌｇｏｒｉｔｈｍｓ ｆｏｒ ｓｏｌｖｉｎｇ ＳＡＴ， ａｎａｌｏｇｏｕｓ ＳＡＴ ａｎｄ ＃ＳＡＴ ｕｓｉｎｇ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ａｒｅ ｍａｉｎｌｙ ａｎａｌｙｚｅｄ． Ｆｉｎａｌｌｙ， ｔｈｅ ｒｅｌａｔｅｄ ｒｅｓｅａｒｃｈ ｈｏｔｓｐｏｔｓ ａｎｄ ｄｅｖｅｌｏｐｉｎｇ ｔｒｅｎｄｓ ａｒｅ ｐｏｉｎｔｅｄ ｏｕｔ． Ｋｅｙｗｏｒｄｓ：ａｕｔｏｍａｔｅｄ ｒｅａｓｏｎｉｎｇ； ｒｅｓｏｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ； ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ； ＳＡＴ； ＃ＳＡＴ 收稿日期：２０１３⁃０８⁃０７． 网络出版日期：２０１４⁃０２⁃２０． 基金项目：国家自然科学基金资助项目（６１０７００８４， ６１２７２５３５， ６１１６３０６５， ６１３７０１５６，６１１６５００９）；国家“９７３”计划资助项目（２０１２ＣＢ３２６４０３）； 广西 自 然 科 学 基 金 资 助 项 目 （ ２０１３ＧＸＮＳＦＢＡ０１９２６３， ２０１２ＧＸＮＳＦＡＡ０５３２１９）；广西高校科研项目（２０１３ＹＢ０２９）； “八桂学者”工程专项经费资助项目；广西师范大学博士启 动基金资助项目． 通信作者：覃少华． Ｅ⁃ｍａｉｌ： ｓｈｑｉｎ＠ ｇｘｎｕ．ｅｄｕ．ｃｎ． 作为数理逻辑中形式化推理的一个分支，自动 推理在人工智能发展初期就引起了研究者的广泛关 注。 定理证明是领域的研究热点，其发展深刻地影 响着人工智能乃至计算机科学的其他研究方向，并 在计算机工程中有着广泛的应用［１］ 。 如在软件验 证和硬件校验方面，Ｋａｒｌｓｒｕｈｅ 大学开发的 ＫＩＶ ［２］ 已 成功用于验证许多应用软件，包括图和树的表示等 实验室软件和用于铁路转弯控制等工业软件，一些 大公司如英特尔、摩托罗拉、ＡＭＤ 等都使用基于定 理证明的硬件校验技术。 在智能规划领域，把规划 问题编译成 ＳＡＴ （ ｓａｔｉｓｆｉａｂｌｉｔｙ） 问题并利用高效的 ＳＡＴ 求解器进行求解已成为一种主要方法。 基于 ＳＡＴ 的规划系统，在两年一度的国际规划器竞赛中 屡获冠军，表现出优异的性能［３］ 。 Ｇｒａｓｔｉｅｎ 等［４］ 将 基于模型的诊断问题转化成 ＳＡＴ 问题，并且利用 ＳＡＴ 求解算法进行诊断。 与传统的方法相比，基于 ＳＡＴ 的诊断方法能解决更复杂的诊断问题

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，…，三相近，由它们构成的集合称为相 进展

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

第1期 王金艳，等：扩展规则方法研究综述 ·3 2.1基于扩展规则的SAT求解方法 的情况下，效率会降低。 2.1.1ER和ER算法 2.1.3基于启发式策略的ER算法 2003年，in等[沿着归结原理的反向提出一 ER算法通过随机选取子句C来限定极大项搜 条新的推理规则一扩展规则，使用扩展规则进行定 索空间，为了尽可能地在该子空间中判定出给定子 理证明的算法ER(theorem proving based on exten- 句集的可满足性，以提高算法的效率，子句C的选 sion rule),其基本思想是把给定的子句集∑扩展成 取至关重要。Lin等在文献[7]中指出，对于具体的 由极大项组成的子句集'，然后根据极大项的个数 问题，通过问题的背景知识来调整子句C的输入可 |∑|来判定Σ的可满足性，如果1∑1=2m(m为 能会提高ER算法的效率，并将C的选取作为一个 的变量数)，则Σ是不可满足的：否则Σ可满足。事 开放问题。 实上并不需要将Σ'扩展出来，只需计算出Σ就 李莹等[18]根据具体给定子句集所包含的信息 可以判定Σ的可满足性。因此他们利用容斥原理 提出了2种用于选择限定搜索空间子句的启发式策 直接计算出|Σ|，降低了该方法的空间复杂性。 IMOM improved maximum occurrences on clauses 一般情况下，ER算法的时间复杂性是指数级的，效 of maximum size)和IBOHM(improved BOHM)。 率比较低，但是在任意2个子句都含有互补对的情 IMOM是优先选择最长子句中出现频率高的文字的 况下，ER算法的效率较高，而使用基于归结的方法 否定加入子句C,IBOHM是优先选择拥有极大向量 效率较低。可以用互补因子C来比较基于扩展规 （H(L,),H2(L,),…,H(L))的文字L加入到子 则的方法和基于归结的方法。假设所有的SAT问 句C中，其中H(L)为子句集中长度为j的包含文字 题都在一个光谱上，其左端是互补因子为1的问题， L的子句个数，并将其分别用于ER算法，提出了 其右端是互补因子为0的问题，在光谱左端用基于 IMOMH_IER和IBOHMH_IER算法。IMOM和IBO- 扩展规则的方法效率更高，而在光谱右端基于归结 HM策略利用子句集的相关信息选择子句C,可以 的方法效率更高。 得到更适合问题的极大项搜索子空间，对于可满足 ER算法实际上是在给定子句集的所有极大项 的问题可以直接返回SAT,不可满足的问题可以较 组成的空间中进行搜索，看是否有不能被扩展出的 早地调用ER算法，减少判定时间，提高了求解效 极大项。为了减少搜索空间提高求解的效率，Lin 率，其平均速度较DR(directional resolution)[6)和 等I7,I]提出了一种高效的算法ER(improved exten- IER算法可以提高10~200倍。 sion rule)。该方法首先在极大项空间的一个子空 2.1.4与归结方法的结合 间中搜索，如果在子空间中有不能被扩展的极大项， 基于扩展规则的方法和基于归结的方法是2种 那么整个空间就有不能被扩展的极大项，这时子句 互补的方法，为了充分利用其各自的推理特点来提 集是可满足的：否则，不能判定子句集的可满足性， 高SAT问题求解的效率，Wu等19]将2种推理方法 需要调用ER算法。ER算法是先运行一个高效但 结合起来，即将有向归结DR和扩展规则方法ER结 不完备的算法，希望它能解决大部分问题，对于无法 合，提出了综合的推理算法DR-ER。该方法利用子 解决的问题再调用完备的ER算法。 句集的互补因子Ce来决定调用DR还是ER。如果 2.1.2带化简规则的ER和ER算法 Ce≥O.5,调用ER进行推理：否则调用DR进行推 通常，有些子句不会影响子句集不可满足性的 理。DR-ER方法的求解效率优于单独使用DR或 判定，可以将之删除，如含纯文字的子句、被蕴含的 ER方法。 子句等。Wu等[6)利用若干化简规则，包括重言 2.1.5避开容斥原理的扩展规则方法 式规则、单文字规则、纯文字规则和包含规则，对ER 利用容斥原理，ER算法可以巧妙地计算给定 和ER算法进行了改进，提出了带化简规则的扩展 子句集可扩展出的极大项个数，解决了指数级的空 规则算法RER(reduced extension rule)和RIER(re- 间需求问题，但是其时间复杂性仍然是指数级的.严 duced improved extension rule with heuristic)。其基 重影响了算法的求解效率，限制其在实际问题中的 本思想是对给定子句集进行化简并对其可满足性进 应用20]。为了避开容斥原理复杂的求解过程，利用 行快速但不完备的判定，如果能判定子句集的可满 扩展规则的特性，研究人员提出了子句集合包含方 足性，则返回判定结果：否则调用ER或ER算法对 法、极大项覆盖方法和碰集方法，下面分别给予介绍。 化简后的子句集进行判定。在大部分情况下，RER 1)子句集合包含方法。 和RER算法都提高效率，仅在化简规则不起作用 2009年，孙吉贵等20)发现一个极大项能被子

２．１ 基于扩展规则的 ＳＡＴ 求解方法 ２．１．１ ＥＲ 和 ＩＥＲ 算法 ２００３ 年，Ｌｉｎ 等［７］ 沿着归结原理的反向提出一 条新的推理规则—扩展规则，使用扩展规则进行定 理证明的算法 ＥＲ（ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ｂａｓｅｄ ｏｎ ｅｘｔｅｎ⁃ ｓｉｏｎ ｒｕｌｅ），其基本思想是把给定的子句集 Σ 扩展成 由极大项组成的子句集 Σ′ ，然后根据极大项的个数 Σ′ 来判定 Σ 的可满足性，如果 ｜ Σ′ ｜ ＝ ２ ｍ （ｍ 为 Σ 的变量数），则 Σ 是不可满足的；否则 Σ 可满足。 事 实上并不需要将 Σ′ 扩展出来，只需计算出 Σ′ 就 可以判定 Σ 的可满足性。 因此他们利用容斥原理 直接计算出 Σ′ ，降低了该方法的空间复杂性。 一般情况下，ＥＲ 算法的时间复杂性是指数级的，效 率比较低，但是在任意 ２ 个子句都含有互补对的情 况下，ＥＲ 算法的效率较高，而使用基于归结的方法 效率较低。 可以用互补因子 ＣＦ 来比较基于扩展规 则的方法和基于归结的方法。 假设所有的 ＳＡＴ 问 题都在一个光谱上，其左端是互补因子为 １ 的问题， 其右端是互补因子为 ０ 的问题，在光谱左端用基于 扩展规则的方法效率更高，而在光谱右端基于归结 的方法效率更高。 ＥＲ 算法实际上是在给定子句集的所有极大项 组成的空间中进行搜索，看是否有不能被扩展出的 极大项。 为了减少搜索空间提高求解的效率，Ｌｉｎ 等［７，１５］提出了一种高效的算法 ＩＥＲ（ ｉｍｐｒｏｖｅｄ ｅｘｔｅｎ⁃ ｓｉｏｎ ｒｕｌｅ）。 该方法首先在极大项空间的一个子空 间中搜索，如果在子空间中有不能被扩展的极大项， 那么整个空间就有不能被扩展的极大项，这时子句 集是可满足的；否则，不能判定子句集的可满足性， 需要调用 ＥＲ 算法。 ＩＥＲ 算法是先运行一个高效但 不完备的算法，希望它能解决大部分问题，对于无法 解决的问题再调用完备的 ＥＲ 算法。 ２．１．２ 带化简规则的 ＥＲ 和 ＩＥＲ 算法 通常，有些子句不会影响子句集不可满足性的 判定，可以将之删除，如含纯文字的子句、被蕴含的 子句等。 Ｗｕ 等［１６⁃１７］ 利用若干化简规则，包括重言 式规则、单文字规则、纯文字规则和包含规则，对 ＥＲ 和 ＩＥＲ 算法进行了改进，提出了带化简规则的扩展 规则算法 ＲＥＲ（ｒｅｄｕｃｅｄ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）和 ＲＩＥＲ（ ｒｅ⁃ ｄｕｃｅｄ ｉｍｐｒｏｖｅｄ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｗｉｔｈ ｈｅｕｒｉｓｔｉｃ）。 其基 本思想是对给定子句集进行化简并对其可满足性进 行快速但不完备的判定，如果能判定子句集的可满 足性，则返回判定结果；否则调用 ＥＲ 或 ＩＥＲ 算法对 化简后的子句集进行判定。 在大部分情况下，ＲＥＲ 和 ＲＩＥＲ 算法都提高效率，仅在化简规则不起作用 的情况下，效率会降低。 ２．１．３ 基于启发式策略的 ＩＥＲ 算法 ＩＥＲ 算法通过随机选取子句 Ｃ 来限定极大项搜 索空间，为了尽可能地在该子空间中判定出给定子 句集的可满足性，以提高算法的效率，子句 Ｃ 的选 取至关重要。 Ｌｉｎ 等在文献［７］中指出，对于具体的 问题，通过问题的背景知识来调整子句 Ｃ 的输入可 能会提高 ＩＥＲ 算法的效率，并将 Ｃ 的选取作为一个 开放问题。 李莹等［１８］根据具体给定子句集所包含的信息 提出了 ２ 种用于选择限定搜索空间子句的启发式策 略 ＩＭＯＭ（ ｉｍｐｒｏｖｅｄ ｍａｘｉｍｕｍ ｏｃｃｕｒｒｅｎｃｅｓ ｏｎ ｃｌａｕｓｅｓ ｏｆ ｍａｘｉｍｕｍ ｓｉｚｅ ） 和 ＩＢＯＨＭ （ ｉｍｐｒｏｖｅｄ ＢＯＨＭ ）。 ＩＭＯＭ 是优先选择最长子句中出现频率高的文字的 否定加入子句 Ｃ，ＩＢＯＨＭ 是优先选择拥有极大向量 （Ｈ１（Ｌｉ）， Ｈ２（Ｌｉ）， …， Ｈｎ（Ｌｉ））的文字 Ｌｉ加入到子 句 Ｃ 中，其中 Ｈｊ（Ｌ）为子句集中长度为 ｊ 的包含文字 Ｌ 的子句个数，并将其分别用于 ＩＥＲ 算法，提出了 ＩＭＯＭＨ＿ＩＥＲ 和 ＩＢＯＨＭＨ＿ＩＥＲ 算法。 ＩＭＯＭ 和 ＩＢＯ⁃ ＨＭ 策略利用子句集的相关信息选择子句 Ｃ，可以 得到更适合问题的极大项搜索子空间，对于可满足 的问题可以直接返回 ＳＡＴ，不可满足的问题可以较 早地调用 ＥＲ 算法，减少判定时间，提高了求解效 率，其平均速度较 ＤＲ （ ｄｉｒｅｃｔｉｏｎａｌ ｒｅｓｏｌｕｔｉｏｎ） ［６］ 和 ＩＥＲ 算法可以提高１０～２００ 倍。 ２．１．４ 与归结方法的结合 基于扩展规则的方法和基于归结的方法是 ２ 种 互补的方法，为了充分利用其各自的推理特点来提 高 ＳＡＴ 问题求解的效率，Ｗｕ 等［ １ ９ ］将 ２ 种推理方法 结合起来，即将有向归结 ＤＲ 和扩展规则方法 ＥＲ 结 合，提出了综合的推理算法 ＤＲ⁃ＥＲ。 该方法利用子 句集的互补因子 ＣＦ 来决定调用 ＤＲ 还是 ＥＲ。 如果 ＣＦ ≥ ０．５，调用 ＥＲ 进行推理；否则调用 ＤＲ 进行推 理。 ＤＲ⁃ＥＲ 方法的求解效率优于单独使用 ＤＲ 或 ＥＲ 方法。 ２．１．５ 避开容斥原理的扩展规则方法 利用容斥原理，ＥＲ 算法可以巧妙地计算给定 子句集可扩展出的极大项个数，解决了指数级的空 间需求问题，但是其时间复杂性仍然是指数级的，严 重影响了算法的求解效率，限制其在实际问题中的 应用［２０］ 。 为了避开容斥原理复杂的求解过程，利用 扩展规则的特性，研究人员提出了子句集合包含方 法、极大项覆盖方法和碰集方法，下面分别给予介绍。 １）子句集合包含方法。 ２００９ 年，孙吉贵等［２０］ 发现一个极大项能被子 第 １ 期 王金艳，等：扩展规则方法研究综述 ·３·

·4 智能系统学报 第9卷 句集扩展出来，子句集中必须有子句包含于该极大 2)极大项覆盖方法。 项（子句看作文字集合）。基于该性质，孙吉贵等提 为了避开容斥原理求解的复杂性，Yin等[2]从 出了一种新的基于扩展规则的定理证明方法NER, 相对极大项角度提出了一种基于极大项覆盖的有效 该方法将SAT问题转化为一系列文字集合的包含 SAT求解方法MC(maxterm covering for satisfiabili- 问题。NER算法按照一定次序判断极大项是否可 y)。子句C关于子句集Σ覆盖的相对极大项是C 被当前待判定的子句集Σ扩展，若存在某个极大项 覆盖，但不是Σ覆盖的极大项，表示为 不能被扩展出来，那么Σ是可满足的：否则，若所有 relativeMaxterm(C,)=MC(C)IMC()。设子句 极大项都可以被扩展出来，则Σ是不可满足的。其 集={C1,C2,C,C4{,C关于Σ的相对极大项如 最优和最坏时间复杂度分别为O(m+n×k2)和 图1所示。 O(2×(m+n×k2)),m、n、k分别表示子句集中变量 的个数、子句的个数和子句的平均长度。实验结果 表明，无论是对于随机问题还是标准测试用例，NER 算法的执行效率较ER和DR算法都有很大的提 高，有些问题可以提高2个数量级。 NER算法将所有极大项按照一定顺序来一一 判定其是否能由子句集扩展出来，直到某个极大项 不能被扩展时或者所有极大项都可由子句集扩展出 来时，才能判定出子句集的可满足性。事实上，当一 个极大项可由某一子句扩展时，接下来的部分极大 relativeMaxterm 项可以不用判断其是否可由子句集扩展出来，从而 (C 减少了需要判断的极大项个数。张立明等2定义 图1C关于的相对极大项 了半扩展规则，并且提出了基于半扩展规则的定理 Fig.1 The relative maxterm of C with respect to 证明方法SRE(semi-extension rule)。SRE算法是在 给定一个变量集合，设所有极大项集合为论域， NER算法的基础上，按一定顺序判定极大项是否可 那么空子句ε覆盖的极大项集合等于该论域。根据 被子句集扩展，当一个极大项可被子句集中的某一 扩展规则方法可知，如果MC()=MC(ε)，则子句 子句扩展时，那么基于此子句半扩展出的所有极大 集∑是不可满足的：如果relativeMaxterm(e,)≠ 项都不需判断其是否可被子句集扩展，这样减少了 ☑，则Σ是可满足的。图2给出了一个可满足的问 需要判断的极大项个数，使计算复杂度由原来NER 题实例。 方法的0(2"×(m+n×k2))降为0(2×(m+n×k2)+ n),其中d为子句集中子句的度的平均值。d越 小，SRE算法的求解效率越高：当d趋近与m时， SRE算法的求解效率较NER算法提高较小。 进一步，他们提出了基于半扩展规则的并行定 理证明方法PPSER(parallel theorem proving algo- rithm based on semi-extension rule)[2a,该方法首先 给出在极大项子空间中判定子句集可满足性的算法 PSER,然后将子句集的极大项空间分解为若干个互 不相交的子空间，对每个极大项子空间，并行地调用 MC relativeMaxterm(a,) PSER方法进行判定，如果有一个极大项子空间中 返回的结果为SAT,即该子空间中存在某个极大项 图2一个可满足问题实例 不能被扩展出来，则子句集是可满足的：否则，如果 Fig.2 A satisfiable example 所有极大项子空间返回的结果都为UNSAT,即所有 MC方法利用空子句关于子句集的相对极大项 极大项都能被扩展出来，那么子句集是不可满足的。 的个数来判定子句集的可满足性。如果相对极大项 由于并行处理，该算法在求解效率上较SRE算法有 个数为0，则子句集是不可满足的：否则，子句集是 了较大的提高。 可满足的。与扩展规则方法根据扩展出的极大项个

句集扩展出来，子句集中必须有子句包含于该极大 项（子句看作文字集合）。 基于该性质，孙吉贵等提 出了一种新的基于扩展规则的定理证明方法 ＮＥＲ， 该方法将 ＳＡＴ 问题转化为一系列文字集合的包含 问题。 ＮＥＲ 算法按照一定次序判断极大项是否可 被当前待判定的子句集 Σ 扩展，若存在某个极大项 不能被扩展出来， 那么 Σ 是可满足的；否则，若所有 极大项都可以被扩展出来，则 Σ 是不可满足的。 其 最优和最坏时间复杂度分别为 Ｏ （ ｍ ＋ ｎ × ｋ ２ ） 和 Ｏ（２ ｍ ×（ｍ＋ｎ×ｋ ２ ）），ｍ、ｎ、ｋ 分别表示子句集中变量 的个数、子句的个数和子句的平均长度。 实验结果 表明，无论是对于随机问题还是标准测试用例，ＮＥＲ 算法的执行效率较 ＩＥＲ 和 ＤＲ 算法都有很大的提 高，有些问题可以提高 ２ 个数量级。 ＮＥＲ 算法将所有极大项按照一定顺序来一一 判定其是否能由子句集扩展出来，直到某个极大项 不能被扩展时或者所有极大项都可由子句集扩展出 来时，才能判定出子句集的可满足性。 事实上，当一 个极大项可由某一子句扩展时，接下来的部分极大 项可以不用判断其是否可由子句集扩展出来，从而 减少了需要判断的极大项个数。 张立明等［２１］ 定义 了半扩展规则，并且提出了基于半扩展规则的定理 证明方法 ＳＲＥ（ｓｅｍｉ⁃ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）。 ＳＲＥ 算法是在 ＮＥＲ 算法的基础上，按一定顺序判定极大项是否可 被子句集扩展，当一个极大项可被子句集中的某一 子句扩展时，那么基于此子句半扩展出的所有极大 项都不需判断其是否可被子句集扩展，这样减少了 需要判断的极大项个数，使计算复杂度由原来 ＮＥＲ 方法的 Ｏ（２ ｍ ×（ｍ＋ｎ×ｋ ２ ））降为 Ｏ（２ ｄ ×（ｍ＋ｎ×ｋ ２ ）＋ ｎ ２ ），其中 ｄ 为子句集中子句的度的平均值。 ｄ 越 小，ＳＲＥ 算法的求解效率越高；当 ｄ 趋近与 ｍ 时， ＳＲＥ 算法的求解效率较 ＮＥＲ 算法提高较小。 进一步，他们提出了基于半扩展规则的并行定 理证明方法 ＰＰＳＥＲ （ ｐａｒａｌｌｅｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ａｌｇｏ⁃ ｒｉｔｈｍ ｂａｓｅｄ ｏｎ ｓｅｍｉ⁃ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） ［２２］ ，该方法首先 给出在极大项子空间中判定子句集可满足性的算法 ＰＳＥＲ，然后将子句集的极大项空间分解为若干个互 不相交的子空间，对每个极大项子空间，并行地调用 ＰＳＥＲ 方法进行判定，如果有一个极大项子空间中 返回的结果为 ＳＡＴ，即该子空间中存在某个极大项 不能被扩展出来，则子句集是可满足的；否则，如果 所有极大项子空间返回的结果都为 ＵＮＳＡＴ，即所有 极大项都能被扩展出来，那么子句集是不可满足的。 由于并行处理，该算法在求解效率上较 ＳＲＥ 算法有 了较大的提高。 ２）极大项覆盖方法。 为了避开容斥原理求解的复杂性，Ｙｉｎ 等［２３］ 从 相对极大项角度提出了一种基于极大项覆盖的有效 ＳＡＴ 求解方法 ＭＣ（ ｍａｘｔｅｒｍ ｃｏｖｅｒｉｎｇ ｆｏｒ ｓａｔｉｓｆｉａｂｉｌｉ⁃ ｔｙ）。 子句 Ｃ 关于子句集 Σ 覆盖的相对极大项是 Ｃ 覆 盖， 但 不 是 Σ 覆 盖 的 极 大 项， 表 示 为 ｒｅｌａｔｉｖｅＭａｘｔｅｒｍ（Ｃ，Σ） ＝ ＭＣ（Ｃ） ＼ＭＣ（Σ） 。 设子句 集 Σ ＝ ｛Ｃ１ ， Ｃ２ ， Ｃ３ ， Ｃ４ ｝，Ｃ 关于 Σ 的相对极大项如 图 １ 所示。 图 １ Ｃ 关于 Σ 的相对极大项 Ｆｉｇ． １ Ｔｈｅ ｒｅｌａｔｉｖｅ ｍａｘｔｅｒｍ ｏｆ Ｃ ｗｉｔｈ ｒｅｓｐｅｃｔ ｔｏ Σ 给定一个变量集合，设所有极大项集合为论域， 那么空子句 ε 覆盖的极大项集合等于该论域。 根据 扩展规则方法可知，如果 ＭＣ（Σ） ＝ ＭＣ（ε） ，则子句 集 Σ 是不可满足的；如果 ｒｅｌａｔｉｖｅＭａｘｔｅｒｍ（ε，Σ） ≠ ∅， 则 Σ 是可满足的。 图 ２ 给出了一个可满足的问 题实例。 图 ２ 一个可满足问题实例 Ｆｉｇ． ２ Ａ ｓａｔｉｓｆｉａｂｌｅ ｅｘａｍｐｌｅ ＭＣ 方法利用空子句关于子句集的相对极大项 的个数来判定子句集的可满足性。 如果相对极大项 个数为 ０，则子句集是不可满足的；否则，子句集是 可满足的。 与扩展规则方法根据扩展出的极大项个 ·４· 智 能 系 统 学 报 第 ９ 卷

第1期 王金艳，等：扩展规则方法研究综述 5 数来判断子句集的可满足性不同，该方法直接计算 现有其他知识编译方法对偶的一种方法2]。 出不能由子句集扩展出来的相对极大项个数，然后 2)基于启发式策略的知识编译方法。 根据相对极大项个数来判断子句集的可满足性，避 在知识编译中，离线编译后生成的目标知识库 开了容斥原理的复杂性。进一步，他们在基本MC 的规模对在线查询的效率起着至关重要的作用。算 算法的基础上提出了8种优化策略，极大地提高了 法KCER在选择子句和变量进行扩展时，都采用顺 算法的求解效率。 序扩展的方式，几乎没有使用任何启发式策略。对 3)碰集方法。 于有些问题，这会导致编译后的子句集规模过大，从 Xu等[242]找出了不能被扩展出的极大项具有 而影响之后的在线推理的效率。为此，笔者提出了 的特征，以此来回避容斥原理所带来的计算量。他 2种启发式策略MCN(minimum complementary num- 们发现，若极大项与子句集Σ中的某个子句互补， ber)和MO(maximum occurrences)分别用于指导待 则该极大项不能由这个子句扩展出来。进而可知， 扩展的子句和变量的选择[]，MCN策略是优先选 如果极大项与Σ中所有子句都互补，那么该极大项 择与其他子句互补的子句数较少的子句进行扩展， 就不能由Σ扩展出来。假定存在与Σ中任意子句 MO策略是在待扩展的子句中优先选择在其他未扩 都互补的极大项C,那么由C,可以构造极大项 展子句中出现次数最多的变量进行扩展。前者使得 CM,其中C,由Cv中每个文字的补文字构成。如果 需要扩展的子句数较少，后者使得子句被扩展出的 将子句看作文字集合，Σ看作文字集合簇，那么C 子句数较少。使用随机生成的样例和处于相变区的 与Σ中任意子句的交都不为空，即C,是Σ的碰集。 Uniform Random-3-SAT标准用例进行测试，实验结 基于此，Xu等证明了子句集是可满足的，当且仅当 果表明，MCN和MO策略都能大幅度地减小编译后 该子句集存在不包含互补文字的碰集，这样就将 的子句集规模，其中MCN的效果比MO更为明显。 SAT问题转化成判定是否存在不含互补文字的碰集 同时使用MCN和MO策略，可以使扩展后的子句集 问题，并且提出了2种有效的方法CBHST(comple- mentary binary hitting set tree)RNHST(revised new 规模为算法KCER的J 3399 hitting set tree)来进行求解。这2种算法与DR相 3)新的EPCCL编译框架。 比，在效率方面都有1~2个数量级的提高。RNHST 赖永[0证明了如下定理：给定子句集∑=1∧ 算法与CBHST算法相比，RNHST更适合长子句的 ,和EPCCL编译算法f,f八∑，)Af(,VΣ2)是 情况，而CBHST更适合短子句的情况。 与Σ等价的EPCCL理论。基于该定理，他提出了一 2.1.6基于扩展规则的知识编译方法 种新的关于EPCCL理论的知识编译思想：对于给定 I)基于KCER的知识编译方法。 的子句集，首先将其划分为2个子句集三，和2，然 Lin和Sum26指出扩展规则方法可以被应用于 后对它们分别进行编译，合取编译后的结果即可得 知识编译列中，他们定义了EPCCL(each pair con- 到与原子句集等价的EPCCL理论。根据划分后 tains complementary literal)理论（任意2个子句都含 I三I、I,I的不同，存在多种划分方式。如何编译 互补对子句集)，证明了EPCCL理论是在“可满足 Σ，V,又分为2种方式。根据子句集的划分方 可控制类”和“蕴含可控制类”中，并证明对于任意 式、∑，V∑2的编译方式和将DNF(disjunctive nor- 子句集一定能找到一个与之等价的EPCCL理论，因 mal form)编译为EPCCL理论的方法的不同，给出多 此EPCCL理论可以作为知识编译的目标语言，进而 种不同的编译方法。 利用“桶删除”的思想提出将给定子句集编译成 由于编译后的EPCCL理论的规模直接影响到 EPCCL理论的算法KCER(knowledge compilation u- 在线查询效率，刘大有等3)定义了一个规约规则， sing the extension rule)。该方法与现有其他知识编 基于该规则提出了用于缩减EPCCL理论规模的算 译方法的不同之处在于：在编译阶段和推理阶段该 法，该算法具有多项式时间复杂度，然后结合基于 方法都是基于扩展规则的，而其他的知识编译方法 DPLL KCDP knowledge compilation based on 都是基于归结原理的：当互补因子较大的时候，该方 DPLL)算法，实现了C2E编译器。实验结果表明， 法得到的子句集规模相对较小，特别地，当待编译的 不论是编译效率还是编译后子句集的规模都优于基 子句集本身就是一个EPCCL理论，用该方法编译后 于KCER的编译器。在目前的基于DPLL的SAT求 的结果就是其本身，而用其他方法编译，结果可能是 解中，存在许多高效的技术，这些技术都能用于改进 指数级大的。因此，该方法被Murray教授看作是与 KCDP的编译效果，提升C2E编译器的性能

数来判断子句集的可满足性不同，该方法直接计算 出不能由子句集扩展出来的相对极大项个数，然后 根据相对极大项个数来判断子句集的可满足性，避 开了容斥原理的复杂性。 进一步，他们在基本 ＭＣ 算法的基础上提出了 ８ 种优化策略，极大地提高了 算法的求解效率。 ３）碰集方法。 Ｘｕ 等［２４⁃２５］找出了不能被扩展出的极大项具有 的特征，以此来回避容斥原理所带来的计算量。 他 们发现，若极大项与子句集 Σ 中的某个子句互补， 则该极大项不能由这个子句扩展出来。 进而可知， 如果极大项与 Σ 中所有子句都互补，那么该极大项 就不能由 Σ 扩展出来。 假定存在与 Σ 中任意子句 都互补的极大项 ＣＭ ，那么由 ＣＭ 可以构造极大项 ＣＭ ′ ，其中 ＣＭ ′ 由 ＣＭ中每个文字的补文字构成。 如果 将子句看作文字集合，Σ 看作文字集合簇，那么 ＣＭ ′ 与 Σ 中任意子句的交都不为空，即 ＣＭ ′ 是 Σ 的碰集。 基于此，Ｘｕ 等证明了子句集是可满足的，当且仅当 该子句集存在不包含互补文字的碰集，这样就将 ＳＡＴ 问题转化成判定是否存在不含互补文字的碰集 问题，并且提出了 ２ 种有效的方法 ＣＢＨＳＴ（ ｃｏｍｐｌｅ⁃ ｍｅｎｔａｒｙ ｂｉｎａｒｙ ｈｉｔｔｉｎｇ ｓｅｔ ｔｒｅｅ）和 ＲＮＨＳＴ（ｒｅｖｉｓｅｄ ｎｅｗ ｈｉｔｔｉｎｇ ｓｅｔ ｔｒｅｅ）来进行求解。 这 ２ 种算法与 ＤＲ 相 比，在效率方面都有 １～２ 个数量级的提高。 ＲＮＨＳＴ 算法与 ＣＢＨＳＴ 算法相比，ＲＮＨＳＴ 更适合长子句的 情况，而 ＣＢＨＳＴ 更适合短子句的情况。 ２．１．６ 基于扩展规则的知识编译方法 １）基于 ＫＣＥＲ 的知识编译方法。 Ｌｉｎ 和 Ｓｕｎ ［２６］指出扩展规则方法可以被应用于 知识编译［２７］ 中，他们定义了 ＥＰＣＣＬ（ ｅａｃｈ ｐａｉｒ ｃｏｎ⁃ ｔａｉｎｓ ｃｏｍｐｌｅｍｅｎｔａｒｙ ｌｉｔｅｒａｌ）理论（任意 ２ 个子句都含 互补对子句集），证明了 ＥＰＣＣＬ 理论是在“可满足 可控制类”和“蕴含可控制类”中，并证明对于任意 子句集一定能找到一个与之等价的 ＥＰＣＣＬ 理论，因 此 ＥＰＣＣＬ 理论可以作为知识编译的目标语言，进而 利用“桶删除” 的思想提出将给定子句集编译成 ＥＰＣＣＬ 理论的算法 ＫＣＥＲ（ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｕ⁃ ｓｉｎｇ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）。 该方法与现有其他知识编 译方法的不同之处在于：在编译阶段和推理阶段该 方法都是基于扩展规则的，而其他的知识编译方法 都是基于归结原理的；当互补因子较大的时候，该方 法得到的子句集规模相对较小，特别地，当待编译的 子句集本身就是一个 ＥＰＣＣＬ 理论，用该方法编译后 的结果就是其本身，而用其他方法编译，结果可能是 指数级大的。 因此，该方法被 Ｍｕｒｒａｙ 教授看作是与 现有其他知识编译方法对偶的一种方法［２８］ 。 ２）基于启发式策略的知识编译方法。 在知识编译中，离线编译后生成的目标知识库 的规模对在线查询的效率起着至关重要的作用。 算 法 ＫＣＥＲ 在选择子句和变量进行扩展时，都采用顺 序扩展的方式，几乎没有使用任何启发式策略。 对 于有些问题，这会导致编译后的子句集规模过大，从 而影响之后的在线推理的效率。 为此，笔者提出了 ２ 种启发式策略 ＭＣＮ（ｍｉｎｉｍｕｍ ｃｏｍｐｌｅｍｅｎｔａｒｙ ｎｕｍ⁃ ｂｅｒ）和 ＭＯ（ｍａｘｉｍｕｍ ｏｃｃｕｒｒｅｎｃｅｓ）分别用于指导待 扩展的子句和变量的选择［２９］ ，ＭＣＮ 策略是优先选 择与其他子句互补的子句数较少的子句进行扩展， ＭＯ 策略是在待扩展的子句中优先选择在其他未扩 展子句中出现次数最多的变量进行扩展。 前者使得 需要扩展的子句数较少，后者使得子句被扩展出的 子句数较少。 使用随机生成的样例和处于相变区的 Ｕｎｉｆｏｒｍ Ｒａｎｄｏｍ⁃３⁃ＳＡＴ 标准用例进行测试，实验结 果表明，ＭＣＮ 和 ＭＯ 策略都能大幅度地减小编译后 的子句集规模，其中 ＭＣＮ 的效果比 ＭＯ 更为明显。 同时使用 ＭＣＮ 和 ＭＯ 策略，可以使扩展后的子句集 规模为算法 ＫＣＥＲ 的 １ ３ ～ １ ３９ 。 ３）新的 ＥＰＣＣＬ 编译框架。 赖永［３０］证明了如下定理：给定子句集 Σ ＝ Σ１ ∧ Σ２ 和 ＥＰＣＣＬ 编译算法 ｆ， ｆ（Σ１ ） ∧ ｆ（ØΣ１ ∨ Σ２ ） 是 与 Σ 等价的 ＥＰＣＣＬ 理论。 基于该定理，他提出了一 种新的关于 ＥＰＣＣＬ 理论的知识编译思想：对于给定 的子句集，首先将其划分为 ２ 个子句集 Σ１和 Σ２ ，然 后对它们分别进行编译，合取编译后的结果即可得 到与原子句集等价的 ＥＰＣＣＬ 理论。 根据划分后 ｜ Σ１ ｜ 、 ｜ Σ２ ｜ 的不同，存在多种划分方式。 如何编译 ØΣ１ ∨ Σ２ 又分为 ２ 种方式。 根据子句集的划分方 式、 ØΣ１ ∨ Σ２ 的编译方式和将 ＤＮＦ（ｄｉｓｊｕｎｃｔｉｖｅ ｎｏｒ⁃ ｍａｌ ｆｏｒｍ）编译为 ＥＰＣＣＬ 理论的方法的不同，给出多 种不同的编译方法。 由于编译后的 ＥＰＣＣＬ 理论的规模直接影响到 在线查询效率，刘大有等［３１］ 定义了一个规约规则， 基于该规则提出了用于缩减 ＥＰＣＣＬ 理论规模的算 法，该算法具有多项式时间复杂度，然后结合基于 ＤＰＬＬ 的 ＫＣＤＰ （ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｂａｓｅｄ ｏｎ ＤＰＬＬ）算法，实现了 Ｃ２Ｅ 编译器。 实验结果表明， 不论是编译效率还是编译后子句集的规模都优于基 于 ＫＣＥＲ 的编译器。 在目前的基于 ＤＰＬＬ 的 ＳＡＴ 求 解中，存在许多高效的技术，这些技术都能用于改进 ＫＣＤＰ 的编译效果，提升 Ｃ２Ｅ 编译器的性能。 第 １ 期 王金艳，等：扩展规则方法研究综述 ·５·

·6* 智能系统学报 第9卷 2.2基于扩展规则的相近SAT求解方法 子句集的一个模型。由此可知，如果子句集扩展出 在实际应用中，通常需要判定仅相差一个子句 的极大项个数为S,那么该子句集有2-S个模型。 的系列子句集的可满足性，即相近SAT问题。如在 基于此，将扩展规则推广到#SAT问题求解中，提出 模型诊断系统和基于SAT的规划方法中，都需要判 了一种基于扩展规则的模型计数方法CER(count-- 断相近SAT问题的可满足性。 ing models using extension rule)。进而证明了 赖永等1o]首先指出ER算法的实现存在以下 EPCCL理论是在“模型计数可控制”类中，因此 不足：对于子句集(II=n),在计算容斥原理的第 EPCCL理论可以作为模型计数知识编译的目标语 i层时，需要搜索C种情况，在实现过程中采用图搜 言，基于KCER算法提出了基于知识编译的模型计 索的策略进行搜索，保存第i层所有不含互补文字 数算法KCCER(knowledge compilation for counting 的子句组合，对空间要求较大：且对任意i个子句组 models using extension rule)【。 合情况，在计算组合中出现的文字数时没有使用重 笔者又进一步研究了如何使用扩展规则求解加 用机制。基于以上不足，他们提出了一种更为高效 权模型计数问题。给定子句集={C,C,…, 的实现策略，在实现过程中采用了回溯法代替图搜 Cn},M={a1,a2,…,am}为其变量集合，则∑的所 索策略，降低了算法的空间需求，同时计算第i层的 有可能的赋值的权之和为 算法ER-i重用之前保存的结果，避免了重复计算。 进而，他们发现将ER算法稍作修改就可以用 WMC(Σ，)=Π(o(a,)+u(a:) i=l 于求解相近SAT问题。对于变量集M上的子句集 基于扩展规则的加权模型计数算法CWER ∑U{Cn+1},其中∑={C1,C2,…,Cn},按照是否包 counting weighted models using extension rule) 含C.将所有由i个子句组成的子句集分为2类： 想是先计算出所有使得子句集Σ为假的模型的权 由Σ中i个子句构成和由Σ中i-1个子句和Cn,构 和W(),这样使得Σ为真的模型的权和为 成，那么容斥原理中的第i层为 WMC(Σ，)-W(一)。其中计算W(一)需要利用 ∑IP,nP…nPI= 容斥原理，当子句集∑中任意2个子句都含互补文 1≤k1<2<…<k≤n+1 字时，不存在使得2个子句同时为假的赋值，这样只 IP∩P2∩…∩PI+ 需要计算容斥原理公式的前n项。基于此，笔者提 1≤k1<2<…<k,≤m ∑1PnPn…nP.nP1l 出基于知识编译的加权模型计数算法KCCWER 1≤k1<k红<…<-1写n knowledge compilation for counting weighted models (1) using extension rule)o 式(1)中后一部分的计算如下：对于Σ的任一含i-1 基于上述4种算法CER、CWER、KCCER、KCC- 个子句的子集r,若∑r互补或者C+1与r中任意 WER,笔者设计了JLU-WMCER系统，与传统的（加 子句互补，则，U{Cn}互补，值为0：否则，利用 权)模型计数求解方法需要找出哪些赋值是给定子 ER-i算法在第i-1层时能够额外地计算出后一部 句集的模型（所有模型的权和）不同，该方法需要找 分的值。对于相近子句集簇(，T),其中∑={C, 出哪些赋值不是子句集的模型（所有使得Σ为假的 C2,…,C},T={C1,C2,…,C},可以一次性 赋值权和)。与ER方法类似，当互补因子较高时， 计算出U{C1}、ΣU{C}所包含的极大项， 基于扩展规则的（加权）模型计数方法一般要优于 从而判定出它们的可满足性。因此提出求解相近 基于归结的方法：当互补因子较低时，基于扩展规则 SAT问题的nER算法。在多数情况下，算法nER求 的方法要差于基于归结的方法，因此可以看作是目 解相近SAT问题的时间仅相当于调用ER算法求解 前其他（加权）模型计数问题求解方法的补方法。 其中一个SAT问题的时间，ER算法的效率远远高 2.3.2避开容斥原理的SAT方法 于相近SAT问题中多个SAT问题单独求解的效率。 1)与归结方法的结合。 2.3基于扩展规则的#SAT求解方法 由于容斥原理的复杂求解过程，降低了CER算 2.3.1利用容斥原理的#SAT方法 法的效率，赖永等利用1Mod(C)1=2m-a和求 笔者对扩展规则进行深入研究，发现赋值与极 解子句集扩展出的极大项个数的容斥原理公式，得 大项之间存在着一一对应的关系。一个赋值使得子 到了IMod()I=Mod(')I-lMod(AC)I, 句集为真，当且仅当它的“非”形式的极大项不能被 其中C∈∑，=1{C},∧一C可以使用单文字 子句集扩展出来，即不能被扩展出的极大项对应于 规则进行化简。在此基础上提出了一种新的基于扩

２．２ 基于扩展规则的相近 ＳＡＴ 求解方法 在实际应用中，通常需要判定仅相差一个子句 的系列子句集的可满足性，即相近 ＳＡＴ 问题。 如在 模型诊断系统和基于 ＳＡＴ 的规划方法中，都需要判 断相近 ＳＡＴ 问题的可满足性。 赖永等［１０］首先指出 ＥＲ 算法的实现存在以下 不足：对于子句集 Σ（ ｜ Σ ｜ ＝ ｎ），在计算容斥原理的第 ｉ 层时，需要搜索 Ｃ ｉ ｎ 种情况，在实现过程中采用图搜 索的策略进行搜索，保存第 ｉ 层所有不含互补文字 的子句组合，对空间要求较大；且对任意 ｉ 个子句组 合情况，在计算组合中出现的文字数时没有使用重 用机制。 基于以上不足，他们提出了一种更为高效 的实现策略，在实现过程中采用了回溯法代替图搜 索策略，降低了算法的空间需求，同时计算第 ｉ 层的 算法 ＥＲ⁃ｉ 重用之前保存的结果，避免了重复计算。 进而，他们发现将 ＥＲ 算法稍作修改就可以用 于求解相近 ＳＡＴ 问题。 对于变量集 Ｍ 上的子句集 Σ ∪ ｛Ｃｎ＋１ ｝ ，其中 Σ ＝ ｛Ｃ１ ，Ｃ２ ，…，Ｃｎ ｝，按照是否包 含 Ｃｎ ＋１将所有由 ｉ 个子句组成的子句集分为 ２ 类： 由 Σ 中 ｉ 个子句构成和由 Σ 中 ｉ－１ 个子句和 Ｃｎ ＋１构 成，那么容斥原理中的第 ｉ 层为 １≤ｋ ∑１ ＜ ｋ２ ＜ … ＜ ｋｉ≤ｎ＋１ ｜ Ｐｋ１ ∩ Ｐｋ２… ∩ Ｐｋｉ ｜ ＝ １≤ｋ ∑１ ＜ ｋ２ ＜ … ＜ ｋｉ≤ｎ ｜ Ｐｋ１ ∩ Ｐｋ２ ∩ … ∩ Ｐｋｉ ｜ ＋ ∑ １≤ｋ１ ＜ ｋ２ ＜ … ＜ ｋｉ －１≤ｎ ｜ Ｐｋ１ ∩ Ｐｋ２ ∩ … ∩ Ｐｋｉ－１ ∩ Ｐｎ＋１ ｜ （１） 式（１）中后一部分的计算如下：对于 Σ 的任一含 ｉ－１ 个子句的子集 ΣΓ ，若 ΣΓ互补或者 Ｃｎ ＋１与 ΣΓ中任意 子句互补，则 ΣΓ ∪ ｛Ｃｎ＋１ ｝ 互补，值为 ０；否则，利用 ＥＲ⁃ｉ 算法在第 ｉ－１ 层时能够额外地计算出后一部 分的值。 对于相近子句集簇（Σ， Γ），其中 Σ ＝ ｛Ｃ１ ， Ｃ２ ，…，Ｃｎ ｝， Γ ＝ ｛Ｃ １ ｎ＋１ ，Ｃ ２ ｎ＋１ ，…，Ｃ ｍ ｎ＋１ ｝ ，可以一次性 计算出 Σ ∪ ｛Ｃ １ ｎ＋１ ｝、 Σ ∪ ｛Ｃ ｍ ｎ＋１ ｝ 所包含的极大项， 从而判定出它们的可满足性。 因此提出求解相近 ＳＡＴ 问题的 ｎＥＲ 算法。 在多数情况下，算法 ｎＥＲ 求 解相近 ＳＡＴ 问题的时间仅相当于调用 ＥＲ 算法求解 其中一个 ＳＡＴ 问题的时间，ｎＥＲ 算法的效率远远高 于相近 ＳＡＴ 问题中多个 ＳＡＴ 问题单独求解的效率。 ２．３ 基于扩展规则的＃ＳＡＴ 求解方法 ２．３．１ 利用容斥原理的＃ＳＡＴ 方法 笔者对扩展规则进行深入研究，发现赋值与极 大项之间存在着一一对应的关系。 一个赋值使得子 句集为真，当且仅当它的“非”形式的极大项不能被 子句集扩展出来，即不能被扩展出的极大项对应于 子句集的一个模型。 由此可知，如果子句集扩展出 的极大项个数为 Ｓ，那么该子句集有 ２ ｍ －Ｓ 个模型。 基于此，将扩展规则推广到＃ＳＡＴ 问题求解中，提出 了一种基于扩展规则的模型计数方法 ＣＥＲ（ ｃｏｕｎｔ⁃ ｉｎｇ ｍｏｄｅｌｓ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ）。 进 而 证 明 了 ＥＰＣＣＬ 理论是在 “ 模型计数可控制” 类中， 因此 ＥＰＣＣＬ 理论可以作为模型计数知识编译的目标语 言，基于 ＫＣＥＲ 算法提出了基于知识编译的模型计 数算法 ＫＣＣＥＲ （ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｆｏｒ ｃｏｕｎｔｉｎｇ ｍｏｄｅｌｓ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） ［３２］ 。 笔者又进一步研究了如何使用扩展规则求解加 权模型计数问题［３３］ 。 给定子句集 Σ ＝ ｛Ｃ１ ，Ｃ２ ，…， Ｃｎ ｝，Ｍ＝ ｛ａ１ ， ａ２ ， …， ａｍ ｝为其变量集合，则 Σ 的所 有可能的赋值的权之和为 ＷＭＣ（ΣＴ ） ＝ ∏ ｍ ｉ ＝ １ （ｗ（ａｉ） ＋ ｗ（Øａｉ）） 基于扩展规则的加权模 型 计 数 算 法 ＣＷＥＲ （ｃｏｕｎｔｉｎｇ ｗｅｉｇｈｔｅｄ ｍｏｄｅｌｓ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）的思 想是先计算出所有使得子句集 Σ 为假的模型的权 和 Ｗ（ ØΣ） ， 这 样 使 得 Σ 为 真 的 模 型 的 权 和 为 ＷＭＣ（ΣＴ ） － Ｗ（ØΣ） 。 其中计算 Ｗ（ØΣ） 需要利用 容斥原理，当子句集 Σ 中任意 ２ 个子句都含互补文 字时，不存在使得 ２ 个子句同时为假的赋值，这样只 需要计算容斥原理公式的前 ｎ 项。 基于此，笔者提 出基于知识编译的加权模型计数算法 ＫＣＣＷＥＲ （ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｆｏｒ ｃｏｕｎｔｉｎｇ ｗｅｉｇｈｔｅｄ ｍｏｄｅｌｓ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）。 基于上述 ４ 种算法 ＣＥＲ、ＣＷＥＲ、ＫＣＣＥＲ、ＫＣＣ⁃ ＷＥＲ，笔者设计了 ＪＬＵ⁃ＷＭＣＥＲ 系统，与传统的（加 权）模型计数求解方法需要找出哪些赋值是给定子 句集的模型（所有模型的权和）不同，该方法需要找 出哪些赋值不是子句集的模型（所有使得 Σ 为假的 赋值权和）。 与 ＥＲ 方法类似，当互补因子较高时， 基于扩展规则的（加权）模型计数方法一般要优于 基于归结的方法；当互补因子较低时，基于扩展规则 的方法要差于基于归结的方法，因此可以看作是目 前其他（加权）模型计数问题求解方法的补方法。 ２．３．２ 避开容斥原理的＃ＳＡＴ 方法 １）与归结方法的结合。 由于容斥原理的复杂求解过程，降低了 ＣＥＲ 算 法的效率，赖永等［９］利用 ｜ Ｍｏｄ（ØＣ） ｜ ＝ ２ ｍ－｜ Ｃ｜ 和求 解子句集扩展出的极大项个数的容斥原理公式，得 到了 ｜ Ｍｏｄ（Σ） ｜ ＝｜ Ｍｏｄ（Σ′） ｜ －｜ Ｍｏｄ（Σ′∧ØＣ） ｜ ， 其中 Ｃ ∈ Σ，Σ′ ＝ Σ ＼｛Ｃ｝，Σ′ ∧ ØＣ 可以使用单文字 规则进行化简。 在此基础上提出了一种新的基于扩 ·６· 智 能 系 统 学 报 第 ９ 卷

第1期 王金艳，等：扩展规则方法研究综述 。7 展规则的SAT求解算法#ER,该算法继承了扩展规 进一步替换对问题逐渐加强，如果任何一步中返回 则方法的优点，能快速求解互补因子较高的问题。 不可满足，则原问题不可满足：如果在某一步返回可 基于归结的算法DPLL[4]主要借助单文字规则提 满足并且解释没有被阻塞，那么原问题是可满足的。 高求解效率，在互补因子较高的情况下，单文字规则 由于PPI算法需要求出满足式映射，即模型，而ER 往往不能发挥作用，因此算法#DPLL效率较低。结 算法只能判定可满足性，不能给出模型。因此他们 合#ER和#DPLL算法的特点，赖永等提出了#CDE 又给出原子被潜在地阻塞的概念，以及2个原子被 算法，该算法根据IMod(∑，∧∑2)I=IMod(∑，)I- 阻塞和被潜在地阻塞之间的关系，并对PPI算法进 IMod(∑，∧E,)I,利用函数SelectClause(∑)从 行修改，提出了基于扩展规则的一阶定理证明方法 Σ中选择适合算法#DPLL的子句集合∑，文中使用 RPPI(revised primal partial instantiation)o 的是选出所有长度小于等于3的子句作为Σ，。当 Wu等[38]指出Lin给出的原子被潜地阻塞的定 函数返回空集时，算法#CDE等价于#ER:当返回 义对新产生子句的条件限制过严，导致RPPI算法 本身时，算法#CDE等价于#DPLL。#CDE算法综合 是不完备的，他们对潜在阻塞进行了重新定义，并且 了#ER和#DPLL的优点，当互补因子较小时，#CDE 提出了一种新的一阶扩展规则算法RFOER(revised 表现出算法#DPLL的优点，当互补因子较大时，表 first-order extension rule),该算法与RPPI算法主要 现出#ER的优点。 有以下3点不同：1)RPPI算法不完备，而RFOER 2)碰集方法。 算法完备；2)RPPI调用的是基本的ER算法，而 针对SAT问题求解算法的效率会随着子句集 RFOER调用的是更为高效的带化简规则和启发式 的规模的增大而迅速降低的问题，许有军等36提出 策略的ER算法；3)RFOER中增加了M-可满足的情 一种间接应用扩展规则求解#SAT问题的MCEHST 形，使得算法可以被更灵活地应用，更适合用于求解 model counting with extension rule and hitting set 实际的问题。 tree)算法。在文献[24]中，他们发现不能被子句集 3.2描述逻辑 扩展出的极大项可以构造出该子句集的一个碰集， 描述逻辑是一种基于对象的知识表示形式化工 即可以根据子句集是否存在不含互补文字的碰集来 具，是一阶谓词逻辑的可判定子集[3]，研究有效的 判定子句集是否为可满足的。任何不能由子句集扩 推理算法是描述逻辑的一个重要研究内容。Zou 展出的极大项都对应于该子句集的一个模型，而且 等[o]将扩展规则推广到描述逻辑ALC的推理中， 该模型正好与子句集的碰集所扩展出的极大项相对 定义了概念扩展规则CER(concept extension rule) 应。MCEHST算法首先得到子句集的所有极小碰 EPCCCL each pair of clausal concept contains 集，然后利用扩展规则计算出这些碰集扩展出的极 liks)理论，即任意2个子句概念都包含链接（概念 大项个数，即模型数。当变量数一定，随着子句数的 链接或关系链接)的规范概念合取式(conjunction 增加，子句集的极小碰集数显著减少。与已存在的 normal concept,.CNC),提出了基于概念扩展规则的 其他#SAT算法比较，当子句数较大且子句较短时， 推理方法，并且证明该方法能在多项式时间内完成 该方法的执行效率较高：但是当子句数较小时，该算 任意EPCCCL理论的可满足性推理和蕴含推理，因 法的执行效率较低。实际应用时，可以根据情况来 此EPCCCL理论可以作为描述逻辑中知识编译的 决定是否选择MCEHST算法。 目标语言。进一步他们提出了基于概念扩展规则的 描述逻辑知识编译方法，该方法首先利用CER 3 扩展规则在其他逻辑中的应用 DLKC算法将CNC公式编译成EPCCCL理论，然后 目前，扩展规则方法已被推广到一阶逻辑、描述 利用基于概念扩展规则的推理方法可以在多项式时 逻辑、模态逻辑、可能性逻辑和多值逻辑，下面分别 间内回答任意查询。 讨论扩展规则方法在这些逻辑中的应用。 3.3模态逻辑 3.1一阶逻辑 模态逻辑为知识工程和并行程序的研究提供了 利用Hooker提出的部分实例化推理方法PPI 一种形式化的途径4)。目前常用的模态推理方法 (primal partial instantiation)[3),Lin等]把扩展规 大致可分为以下2种：一种是直接推广经典的推理 则方法从命题逻辑提升到一阶逻辑。PPI算法的基 方法使之能应用于模态逻辑：另一种是利用转换方 本思想是把一阶逻辑的定理证明问题转化成一系列 法将模态逻辑转换为经典逻辑，然后利用经典逻辑 SAT问题，首先从较弱的SAT问题入手，然后通过 中的方法进行推理，其中关系转换方法、函数转换方

展规则的＃ＳＡＴ 求解算法＃ＥＲ，该算法继承了扩展规 则方法的优点，能快速求解互补因子较高的问题。 基于归结的算法＃ＤＰＬＬ ［３４⁃３５］主要借助单文字规则提 高求解效率，在互补因子较高的情况下，单文字规则 往往不能发挥作用，因此算法＃ＤＰＬＬ效率较低。 结 合＃ＥＲ 和＃ＤＰＬＬ 算法的特点，赖永等提出了＃ＣＤＥ 算法，该算法根据 ｜ Ｍｏｄ（Σ１ ∧ Σ２） ｜ ＝ ｜ Ｍｏｄ（Σ１） ｜ － ｜ Ｍｏｄ（Σ１ ∧ ØΣ２ ） ｜ ，利用函数 ＳｅｌｅｃｔＣｌａｕｓｅ（Σ） 从 Σ 中选择适合算法＃ＤＰＬＬ 的子句集合 Σ１ ，文中使用 的是选出所有长度小于等于 ３ 的子句作为 Σ１ 。 当 函数返回空集时，算法＃ＣＤＥ 等价于＃ＥＲ；当返回 Σ 本身时，算法＃ＣＤＥ 等价于＃ＤＰＬＬ。 ＃ＣＤＥ 算法综合 了＃ＥＲ 和＃ＤＰＬＬ 的优点，当互补因子较小时，＃ＣＤＥ 表现出算法＃ＤＰＬＬ 的优点，当互补因子较大时，表 现出＃ＥＲ 的优点。 ２）碰集方法。 针对＃ＳＡＴ 问题求解算法的效率会随着子句集 的规模的增大而迅速降低的问题，许有军等［３６］ 提出 一种间接应用扩展规则求解＃ＳＡＴ 问题的 ＭＣＥＨＳＴ （ ｍｏｄｅｌ ｃｏｕｎｔｉｎｇ ｗｉｔｈ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ａｎｄ ｈｉｔｔｉｎｇ ｓｅｔ ｔｒｅｅ）算法。 在文献［２４］中，他们发现不能被子句集 扩展出的极大项可以构造出该子句集的一个碰集， 即可以根据子句集是否存在不含互补文字的碰集来 判定子句集是否为可满足的。 任何不能由子句集扩 展出的极大项都对应于该子句集的一个模型，而且 该模型正好与子句集的碰集所扩展出的极大项相对 应。 ＭＣＥＨＳＴ 算法首先得到子句集的所有极小碰 集，然后利用扩展规则计算出这些碰集扩展出的极 大项个数，即模型数。 当变量数一定，随着子句数的 增加，子句集的极小碰集数显著减少。 与已存在的 其他＃ＳＡＴ 算法比较，当子句数较大且子句较短时， 该方法的执行效率较高；但是当子句数较小时，该算 法的执行效率较低。 实际应用时，可以根据情况来 决定是否选择 ＭＣＥＨＳＴ 算法。 ３ 扩展规则在其他逻辑中的应用 目前，扩展规则方法已被推广到一阶逻辑、描述 逻辑、模态逻辑、可能性逻辑和多值逻辑，下面分别 讨论扩展规则方法在这些逻辑中的应用。 ３．１ 一阶逻辑 利用 Ｈｏｏｋｅｒ 提出的部分实例化推理方法 ＰＰＩ （ｐｒｉｍａｌ ｐａｒｔｉａｌ ｉｎｓｔａｎｔｉａｔｉｏｎ） ［３７］ ，Ｌｉｎ 等［７］ 把扩展规 则方法从命题逻辑提升到一阶逻辑。 ＰＰＩ 算法的基 本思想是把一阶逻辑的定理证明问题转化成一系列 ＳＡＴ 问题，首先从较弱的 ＳＡＴ 问题入手，然后通过 进一步替换对问题逐渐加强，如果任何一步中返回 不可满足，则原问题不可满足；如果在某一步返回可 满足并且解释没有被阻塞，那么原问题是可满足的。 由于 ＰＰＩ 算法需要求出满足式映射，即模型，而 ＥＲ 算法只能判定可满足性，不能给出模型。 因此他们 又给出原子被潜在地阻塞的概念，以及 ２ 个原子被 阻塞和被潜在地阻塞之间的关系，并对 ＰＰＩ 算法进 行修改，提出了基于扩展规则的一阶定理证明方法 ＲＰＰＩ（ｒｅｖｉｓｅｄ ｐｒｉｍａｌ ｐａｒｔｉａｌ ｉｎｓｔａｎｔｉａｔｉｏｎ）。 Ｗｕ 等［３８］指出 Ｌｉｎ 给出的原子被潜地阻塞的定 义对新产生子句的条件限制过严，导致 ＲＰＰＩ 算法 是不完备的，他们对潜在阻塞进行了重新定义，并且 提出了一种新的一阶扩展规则算法 ＲＦＯＥＲ（ｒｅｖｉｓｅｄ ｆｉｒｓｔ⁃ｏｒｄｅｒ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ），该算法与 ＲＰＰＩ 算法主要 有以下 ３ 点不同：１） ＲＰＰＩ 算法不完备，而 ＲＦＯＥＲ 算法完备；２） ＲＰＰＩ 调用的是基本的 ＥＲ 算法，而 ＲＦＯＥＲ 调用的是更为高效的带化简规则和启发式 策略的 ＥＲ 算法；３）ＲＦＯＥＲ 中增加了 Ｍ⁃可满足的情 形，使得算法可以被更灵活地应用，更适合用于求解 实际的问题。 ３．２ 描述逻辑 描述逻辑是一种基于对象的知识表示形式化工 具，是一阶谓词逻辑的可判定子集［３９］ ，研究有效的 推理算法是描述逻辑的一个重要研究内容。 Ｚｏｕ 等［４０］将扩展规则推广到描述逻辑 ＡＬＣ 的推理中， 定义了概念扩展规则 ＣＥＲ（ ｃｏｎｃｅｐｔ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） 和 ＥＰＣＣＣＬ （ ｅａｃｈ ｐａｉｒ ｏｆ ｃｌａｕｓａｌ ｃｏｎｃｅｐｔ ｃｏｎｔａｉｎｓ ｌｉｎｋｓ）理论，即任意 ２ 个子句概念都包含链接（概念 链接或关系链接） 的规范概念合取式（ ｃｏｎｊｕｎｃｔｉｏｎ ｎｏｒｍａｌ ｃｏｎｃｅｐｔ， ＣＮＣ），提出了基于概念扩展规则的 推理方法，并且证明该方法能在多项式时间内完成 任意 ＥＰＣＣＣＬ 理论的可满足性推理和蕴含推理，因 此 ＥＰＣＣＣＬ 理论可以作为描述逻辑中知识编译的 目标语言。 进一步他们提出了基于概念扩展规则的 描述逻辑知识编译方法， 该方法首先利用 ＣＥＲ⁃ ＤＬＫＣ 算法将 ＣＮＣ 公式编译成 ＥＰＣＣＣＬ 理论，然后 利用基于概念扩展规则的推理方法可以在多项式时 间内回答任意查询。 ３．３ 模态逻辑 模态逻辑为知识工程和并行程序的研究提供了 一种形式化的途径［４１］ 。 目前常用的模态推理方法 大致可分为以下 ２ 种：一种是直接推广经典的推理 方法使之能应用于模态逻辑；另一种是利用转换方 法将模态逻辑转换为经典逻辑，然后利用经典逻辑 中的方法进行推理，其中关系转换方法、函数转换方 第 １ 期 王金艳，等：扩展规则方法研究综述 ·７·

8 智能系统学报 第9卷 法等是常用的转换方法。 知识编译算法SPL-KCER将任意给定的可能性知识 Wu等42]利用破坏性方法直接把扩展规则方法 库编译成EPPCCCL理论，然后利用上述的可能性 推广到模态逻辑中，提出了模态系统K中的破坏性 扩展规则方法可以在多项式时间内完成推理。与可 扩展规则方法DMKER(destructive extension rule in 能性归结方法相比，该方法在有些情况下具有独特 modal logic K),该方法将利用化简规则进行简化和 的优势，当待编译的可能性知识库本身就是一个 利用扩展规则判定不可满足性结合在一起，交替进 EPPCCCL理论，新方法编译后的结果就是它本身， 行。DMKER算法能够快速地证明模态系统K中的 而可能性归结方法的结果一般为指数级别的。 所有公理和四类标准的benchmark问题。该方法继 3.5多值逻辑 承了扩展规则方法的优点，当存在较多的互补公式 经典逻辑对知识的表示能力是有限的，多值逻 时，模态逻辑推理的效率明显提高。此外，Wu等) 辑具有更强的表达能力。在许多领域中，不仅需要 分别将关系转换方法、函数转换方法与扩展规则方 布尔变量，而且需要多值变量来表示实体的一些属 法相结合，提出了关系扩展规则方法MRER(modal 性，直接向经典的命题公式中加入多值变量可能会 relational extension rule)、连续模态逻辑中的函数扩 增加原始问题的求解难度，笔者将扩展规则推广到 展规则方法MFER(modal functional extension rule) 多值逻辑中，提出了一种基于扩展规则的多值推理 和非连续模态逻辑的广义函数扩展规则方法GM- 方法[6。这里关注的是标记逻辑，因为任意一个多 FER(general modal functional extension rule)o 值逻辑知识库，都可以找到一个与之等价的标记逻 3.4可能性逻辑 辑知识库，反之亦然。文中定义了标记扩展规则以 可能性逻辑是适用于给定知识中含有不确定因 及最大项的概念，并且利用容斥原理来计算给定标 素或者给定知识不完全一致的情况下进行知识表示 记子句集所扩展出的最大项个数来判定标记子句集 和推理的逻辑。在可能性逻辑中，最主要和最基本 的可满足性。在此基础上定义了标记EPCCL(s 的推理规则是基于Dubois和Prade提出的可能性归 EPCCL)理论，即对于一个带有标记文字的子句集， 结原理[]。笔者将扩展规则方法引入到可能性逻 其中每一对子句都含有互补文字，或者是互补的布 辑中)，定义了可能性包含规则和可能性扩展规 尔文字，或者是互补的标记文字，并且证明s-EPCCL 则，并且提出了基于可能性扩展规则的推理方法，即 理论是在标记可满足可控制类和标记蕴含可控制类 利用可能性扩展规则计算可能性知识库Σ的不一 中，因此，s-EPCCL理论可以作为多值逻辑知识编译 致程度。该方法的基本思想是：首先按照可能性子 的目标语言。笔者提出了一种基于扩展规则的多值 句的权值α对可能性知识库Σ，中的子句从小到大 知识编译方法，该方法首先利用SKCER算法将标记 进行排序，然后顺次考虑Σ的不同α截集Σ。，利用 知识库编译成一个与之等价的s-EPCCL理论，然后 公式ER算法判断Σ的可满足性：如果∑，不可满 利用上述基于扩展规则的多值推理方法可以在多项 足，则三的不一致程度为α，否则继续考虑下一截 式时间内回答查询。 集。与命题逻辑中的扩展规则方法ER类似，对于 4 互补因子较高的问题可能性扩展规则方法效率较 待解决的问题 高，而对于互补因子较低的问题可能性归结方法的 扩展规则方法以其独特的优势使之成为自动推 效率较高，因此，可能性扩展规则方法可以看作是任 理的重要方法之一，目前还存在一些未解决的问题， 何可能性归结方法的补方法。 值得研究人员进一步探讨。 进一步，笔者扩展了经典逻辑的蕴含可控制类 1)如何利用扩展规则方法求解隐蔽集。 和可满足可控制类的概念，定义了可能性蕴含可控 隐蔽集是SAT问题的一个重要结构，与求解难 制类和不一致性程度计算可控制类。在可能性扩展 度有很大的关系，隐蔽集的选择使得剩下的问题能 规则的基础上，笔者提出了EPPCCCL(each pair of 在多项式时间内求解。由于利用扩展规则方法和 possibilistic clauses contains complementary literals) EPCCL理论是可以在多项式时间内判定可满足性 论，即任意2个可能性子句的经典投影都含有互补 的，如何求解隐蔽集使得剩下的问题都是EPCCL理 对的可能性子句集，证明了该理论是在最优化形式 论，是需要进一步研究的问题。 蕴含可控制类和不一致性程度计算可控制类中的， 2)如何选择ER算法的子句C使之与骨架集 可以作为可能性知识编译的目标语言，并且给出了 相对应。 一种可能性知识编译方法。该方法首先利用可能性 骨架集也是SAT问题中的一个重要结构，它是

法等是常用的转换方法。 Ｗｕ 等［４２］利用破坏性方法直接把扩展规则方法 推广到模态逻辑中，提出了模态系统 Ｋ 中的破坏性 扩展规则方法 ＤＭＫＥＲ（ ｄｅｓｔｒｕｃｔｉｖｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｉｎ ｍｏｄａｌ ｌｏｇｉｃ Ｋ），该方法将利用化简规则进行简化和 利用扩展规则判定不可满足性结合在一起，交替进 行。 ＤＭＫＥＲ 算法能够快速地证明模态系统 Ｋ 中的 所有公理和四类标准的 ｂｅｎｃｈｍａｒｋ 问题。 该方法继 承了扩展规则方法的优点，当存在较多的互补公式 时，模态逻辑推理的效率明显提高。 此外，Ｗｕ 等［４３］ 分别将关系转换方法、函数转换方法与扩展规则方 法相结合，提出了关系扩展规则方法 ＭＲＥＲ（ｍｏｄａｌ ｒｅｌａｔｉｏｎａｌ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）、连续模态逻辑中的函数扩 展规则方法 ＭＦＥＲ（ｍｏｄａｌ ｆｕｎｃｔｉｏｎａｌ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ） 和非连续模态逻辑的广义函数扩展规则方法 ＧＭ⁃ ＦＥＲ（ｇｅｎｅｒａｌ ｍｏｄａｌ ｆｕｎｃｔｉｏｎａｌ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ）。 ３．４ 可能性逻辑 可能性逻辑是适用于给定知识中含有不确定因 素或者给定知识不完全一致的情况下进行知识表示 和推理的逻辑。 在可能性逻辑中，最主要和最基本 的推理规则是基于 Ｄｕｂｏｉｓ 和 Ｐｒａｄｅ 提出的可能性归 结原理［４４］ 。 笔者将扩展规则方法引入到可能性逻 辑中［４５］ ，定义了可能性包含规则和可能性扩展规 则，并且提出了基于可能性扩展规则的推理方法，即 利用可能性扩展规则计算可能性知识库 Σ 的不一 致程度。 该方法的基本思想是：首先按照可能性子 句的权值 α 对可能性知识库 Σｐ中的子句从小到大 进行排序，然后顺次考虑 Σｐ的不同 α 截集 Σα ，利用 公式 ＥＲ 算法判断 Σα 的可满足性：如果 Σα 不可满 足，则 Σｐ的不一致程度为 α，否则继续考虑下一截 集。 与命题逻辑中的扩展规则方法 ＥＲ 类似，对于 互补因子较高的问题可能性扩展规则方法效率较 高，而对于互补因子较低的问题可能性归结方法的 效率较高，因此，可能性扩展规则方法可以看作是任 何可能性归结方法的补方法。 进一步，笔者扩展了经典逻辑的蕴含可控制类 和可满足可控制类的概念，定义了可能性蕴含可控 制类和不一致性程度计算可控制类。 在可能性扩展 规则的基础上，笔者提出了 ＥＰＰＣＣＣＬ（ ｅａｃｈ ｐａｉｒ ｏｆ ｐｏｓｓｉｂｉｌｉｓｔｉｃ ｃｌａｕｓｅｓ ｃｏｎｔａｉｎｓ ｃｏｍｐｌｅｍｅｎｔａｒｙ ｌｉｔｅｒａｌｓ）理 论，即任意 ２ 个可能性子句的经典投影都含有互补 对的可能性子句集，证明了该理论是在最优化形式 蕴含可控制类和不一致性程度计算可控制类中的， 可以作为可能性知识编译的目标语言，并且给出了 一种可能性知识编译方法。 该方法首先利用可能性 知识编译算法 ＳＰＬ⁃ＫＣＥＲ 将任意给定的可能性知识 库编译成 ＥＰＰＣＣＣＬ 理论，然后利用上述的可能性 扩展规则方法可以在多项式时间内完成推理。 与可 能性归结方法相比，该方法在有些情况下具有独特 的优势，当待编译的可能性知识库本身就是一个 ＥＰＰＣＣＣＬ 理论，新方法编译后的结果就是它本身， 而可能性归结方法的结果一般为指数级别的。 ３．５ 多值逻辑 经典逻辑对知识的表示能力是有限的，多值逻 辑具有更强的表达能力。 在许多领域中，不仅需要 布尔变量，而且需要多值变量来表示实体的一些属 性，直接向经典的命题公式中加入多值变量可能会 增加原始问题的求解难度，笔者将扩展规则推广到 多值逻辑中，提出了一种基于扩展规则的多值推理 方法［４６］ 。 这里关注的是标记逻辑，因为任意一个多 值逻辑知识库，都可以找到一个与之等价的标记逻 辑知识库，反之亦然。 文中定义了标记扩展规则以 及最大项的概念，并且利用容斥原理来计算给定标 记子句集所扩展出的最大项个数来判定标记子句集 的可满足性。 在此基础上定义了标记 ＥＰＣＣＬ （ ｓ⁃ ＥＰＣＣＬ）理论，即对于一个带有标记文字的子句集， 其中每一对子句都含有互补文字，或者是互补的布 尔文字，或者是互补的标记文字，并且证明 ｓ⁃ＥＰＣＣＬ 理论是在标记可满足可控制类和标记蕴含可控制类 中，因此，ｓ⁃ＥＰＣＣＬ 理论可以作为多值逻辑知识编译 的目标语言。 笔者提出了一种基于扩展规则的多值 知识编译方法，该方法首先利用 ＳＫＣＥＲ 算法将标记 知识库编译成一个与之等价的 ｓ⁃ＥＰＣＣＬ 理论，然后 利用上述基于扩展规则的多值推理方法可以在多项 式时间内回答查询。 ４ 待解决的问题 扩展规则方法以其独特的优势使之成为自动推 理的重要方法之一，目前还存在一些未解决的问题， 值得研究人员进一步探讨。 １）如何利用扩展规则方法求解隐蔽集。 隐蔽集是 ＳＡＴ 问题的一个重要结构，与求解难 度有很大的关系，隐蔽集的选择使得剩下的问题能 在多项式时间内求解。 由于利用扩展规则方法和 ＥＰＣＣＬ 理论是可以在多项式时间内判定可满足性 的，如何求解隐蔽集使得剩下的问题都是 ＥＰＣＣＬ 理 论，是需要进一步研究的问题。 ２）如何选择 ＩＥＲ 算法的子句 Ｃ 使之与骨架集 相对应。 骨架集也是 ＳＡＴ 问题中的一个重要结构，它是 ·８· 智 能 系 统 学 报 第 ９ 卷

第1期 王金艳，等：扩展规则方法研究综述 9 一个变量集合，在每一个模型中这些变量的赋值都 5ROBINSON J A.A machine oriented logic based on the res- 相同。ER算法利用子句C来选择一个极大项空间 olution principleJ.Computer Machine,1965,12 (1 ) 中的子空间来进行搜索，由于不能扩展出的极大项 23-41. 与模型之间存在一一对应的关系，如果将骨架变量 [6]DECHTER R,RISH I.Directional resolution:the Davis- 赋值的非作为子句C,那么对于可满足问题，C限定 Putnam procedure,revisited [C]//Proceedings of the 4th 的子空间中肯定有不能扩展出的极大项。 International Conference on Principles of Knowledge Repre- sentation and Reasoning.Bonn,Germany,1994:134-145 3)探求扩展规则方法在其他逻辑中的应用。 [7]LIN Hai,SUN Jigui,ZHANG Yimin.Theorem proving 目前，研究者主要集中于命题逻辑中扩展规则 based on the extension rule J.Journal of Automated Rea- 方法的研究，而在其他逻辑中的研究甚少，在可能性 soning,2003,31(1):11-21. 逻辑、多值逻辑等中，只是将最基本的ER算法进行 [8]DAVIS M,PUTNAM H.A computing procedure for quanti- 推广。由于ER算法利用容斥原理进行推理，严重 fication theory[J].Journal of the ACM,1960,7(3):201- 影响算法的求解效率。因此，在上述逻辑中扩展规 215 则方法的效率还有很大的提升空间。另外，还可以 [9]DAVIS M,LOGEMANN G,LOVELAND D.A machine 考虑将扩展规则方法推广到模糊逻辑、概率逻辑等 program for theorem-proving[J].Communications of the 其他逻辑中。 ACM,1962,5(7):394-397. [10]赖永，欧阳丹彤，蔡敦波，等.基于扩展规则的模型计数 5结束语 与智能规划方法[J].计算机研究与发展，2009,46 扩展规则方法是与归结方法对称的一种自动推 (3):459-469. 理方法，它的提出为自动推理的研究提供了新的研 LAI Yong,OUYANG Dantong,CAI Dunbo,et al.Model 究角度，注入了新的活力。本文较全面地介绍了扩 counting and planning using extension rule[J].Journal of Computer Research and Development,2009,46(3):459- 展规则方法的发展，包括相关概念、各种基于扩展规 469 则的求解方法以及待解决的问题，主要围绕命题逻 [11]SANG T,BEAME P,KAUTZ H.Solving Bayesian net- 辑中的各种扩展规则方法进行分析，并讨论了扩展 works by weighted model counting[C]//Proceedings of the 规则方法在其他逻辑中的应用。尽管目前扩展规则 Twentieth National Conference on Artificial Intelligence. 方法的研究取得了一定的成果，但是在算法的提升、 Pittsburgh,USA,2005:475-482. 各种逻辑的应用方面仍有很大的研究空间。 [12]谷文祥，李淑霞，殷明浩.隐蔽集的研究及发展[J]计算 参考文献： 机科学，2010,37(3)：11-16. GU Wenxiang,LI Shuxia,YIN Minghao.Research and de- [1]殷明浩.自动推理和智能规划中若干问题研究[D].长 velopment in backdoor set[J].Computer Science,2010, 春：吉林大学，2008：1-109. 37(3):11-16. YIN Minghao.The research on several issues of automated [13]NISHIMURA N,RAGDE P,SZEIDER S.Detecting back- reasoning and artificial intelligent planning D.Chang- door sets with respect to Homn and binary clauses[C] chun:Jilin University,2008:1-109. Proceedings of the 7th International Conference on Theory [2]WOLFGANG R.The KIV system:systematic construction of and Applications of Satisfiability Testing.Vancouver,Can- verified software[C]//Proceedings of the 11th International ada,2004:96-103. Conference on Automated Deduction.Saratoga Springs, [14]MNASSON N,ZECCHINA R,KIRKPATRICK S.Deter- USA,1992:753-757. mining computational complexity form characteristic 「3]吕帅，刘磊，石莲，等.基于自动推理技术的智能规划方法 'phase transitions'[J].Nature,1999,400:133-137. [J].软件学报，2009,20(5)：1226-1240 [15]林海.基于扩展规则的定理证明和知识编译[D].长春： LU Shuai,LIU Lei,SHI Lian,et al.Artificial intelligence 吉林大学，2003：140. planning methods based on automated reasoning techniques LIN Hai.Theorem proving and knowledge compilation J].Journal of Software,2009,20(5):1226-1240. based on the extension rule D.Changchun:Jilin Univer- [4]GRASTIEN A,ANBULAGAN A,RINTANEN J,et al.Di- 8ity,2003:1-40. agnosis of discrete-event systems using satisfiability algo- [16]WU Xia,SUN Jigui,LU Shuai,et al.Improved proposi- rithms[C]//Proceedings of the Twenty-Second Conference tional extension rule[C]//Proceedings of the First Interna- on Artificial Intelligence.Vancouver,Canada,2007:305- tional Conference on Rough Sets and Knowledge Technolo- 310. gy.Chongqing,China,2006:592-597

一个变量集合，在每一个模型中这些变量的赋值都 相同。 ＩＥＲ 算法利用子句 Ｃ 来选择一个极大项空间 中的子空间来进行搜索，由于不能扩展出的极大项 与模型之间存在一一对应的关系，如果将骨架变量 赋值的非作为子句 Ｃ，那么对于可满足问题，Ｃ 限定 的子空间中肯定有不能扩展出的极大项。 ３）探求扩展规则方法在其他逻辑中的应用。 目前，研究者主要集中于命题逻辑中扩展规则 方法的研究，而在其他逻辑中的研究甚少，在可能性 逻辑、多值逻辑等中，只是将最基本的 ＥＲ 算法进行 推广。 由于 ＥＲ 算法利用容斥原理进行推理，严重 影响算法的求解效率。 因此，在上述逻辑中扩展规 则方法的效率还有很大的提升空间。 另外，还可以 考虑将扩展规则方法推广到模糊逻辑、概率逻辑等 其他逻辑中。 ５ 结束语 扩展规则方法是与归结方法对称的一种自动推 理方法，它的提出为自动推理的研究提供了新的研 究角度，注入了新的活力。 本文较全面地介绍了扩 展规则方法的发展，包括相关概念、各种基于扩展规 则的求解方法以及待解决的问题，主要围绕命题逻 辑中的各种扩展规则方法进行分析，并讨论了扩展 规则方法在其他逻辑中的应用。 尽管目前扩展规则 方法的研究取得了一定的成果，但是在算法的提升、 各种逻辑的应用方面仍有很大的研究空间。 参考文献： ［１］殷明浩．自动推理和智能规划中若干问题研究［Ｄ］．长 春： 吉林大学， ２００８： １⁃１０９． ＹＩＮ Ｍｉｎｇｈａｏ． Ｔｈｅ ｒｅｓｅａｒｃｈ ｏｎ ｓｅｖｅｒａｌ ｉｓｓｕｅｓ ｏｆ ａｕｔｏｍａｔｅｄ ｒｅａｓｏｎｉｎｇ ａｎｄ ａｒｔｉｆｉｃｉａｌ ｉｎｔｅｌｌｉｇｅｎｔ ｐｌａｎｎｉｎｇ［Ｄ］． Ｃｈａｎｇ⁃ ｃｈｕｎ： Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， ２００８： １⁃１０９． ［２］ＷＯＬＦＧＡＮＧ Ｒ． Ｔｈｅ ＫＩＶ ｓｙｓｔｅｍ： ｓｙｓｔｅｍａｔｉｃ ｃｏｎｓｔｒｕｃｔｉｏｎ ｏｆ ｖｅｒｉｆｉｅｄ ｓｏｆｔｗａｒｅ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １１ｔｈ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｕｔｏｍａｔｅｄ Ｄｅｄｕｃｔｉｏｎ． Ｓａｒａｔｏｇａ Ｓｐｒｉｎｇｓ， ＵＳＡ， １９９２： ７５３⁃７５７． ［３］吕帅，刘磊，石莲，等．基于自动推理技术的智能规划方法 ［Ｊ］．软件学报， ２００９， ２０（５）： １２２６⁃１２４０． ＬＵ Ｓｈｕａｉ， ＬＩＵ Ｌｅｉ， ＳＨＩ Ｌｉａｎ， ｅｔ ａｌ． Ａｒｔｉｆｉｃｉａｌ ｉｎｔｅｌｌｉｇｅｎｃｅ ｐｌａｎｎｉｎｇ ｍｅｔｈｏｄｓ ｂａｓｅｄ ｏｎ ａｕｔｏｍａｔｅｄ ｒｅａｓｏｎｉｎｇ ｔｅｃｈｎｉｑｕｅｓ ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔｗａｒｅ， ２００９， ２０（５）： １２２６⁃１２４０． ［４］ＧＲＡＳＴＩＥＮ Ａ， ＡＮＢＵＬＡＧＡＮ Ａ， ＲＩＮＴＡＮＥＮ Ｊ， ｅｔ ａｌ． Ｄｉ⁃ ａｇｎｏｓｉｓ ｏｆ ｄｉｓｃｒｅｔｅ⁃ｅｖｅｎｔ ｓｙｓｔｅｍｓ ｕｓｉｎｇ ｓａｔｉｓｆｉａｂｉｌｉｔｙ ａｌｇｏ⁃ ｒｉｔｈｍｓ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ Ｔｗｅｎｔｙ⁃Ｓｅｃｏｎｄ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ． Ｖａｎｃｏｕｖｅｒ， Ｃａｎａｄａ， ２００７： ３０５⁃ ３１０． ［５］ＲＯＢＩＮＳＯＮ Ｊ Ａ． Ａ ｍａｃｈｉｎｅ ｏｒｉｅｎｔｅｄ ｌｏｇｉｃ ｂａｓｅｄ ｏｎ ｔｈｅ ｒｅｓ⁃ ｏｌｕｔｉｏｎ ｐｒｉｎｃｉｐｌｅ ［ Ｊ］． Ｃｏｍｐｕｔｅｒ Ｍａｃｈｉｎｅ， １９６５， １２ （ １）： ２３⁃４１． ［６］ ＤＥＣＨＴＥＲ Ｒ， ＲＩＳＨ Ｉ． Ｄｉｒｅｃｔｉｏｎａｌ ｒｅｓｏｌｕｔｉｏｎ： ｔｈｅ Ｄａｖｉｓ⁃ Ｐｕｔｎａｍ ｐｒｏｃｅｄｕｒｅ， ｒｅｖｉｓｉｔｅｄ ［ Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ４ｔｈ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｐｒｉｎｃｉｐｌｅｓ ｏｆ Ｋｎｏｗｌｅｄｇｅ Ｒｅｐｒｅ⁃ ｓｅｎｔａｔｉｏｎ ａｎｄ Ｒｅａｓｏｎｉｎｇ． Ｂｏｎｎ， Ｇｅｒｍａｎｙ， １９９４： １３４⁃１４５． ［７］ ＬＩＮ Ｈａｉ， ＳＵＮ Ｊｉｇｕｉ， ＺＨＡＮＧ Ｙｉｍｉｎ． Ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ｂａｓｅｄ ｏｎ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ａｕｔｏｍａｔｅｄ Ｒｅａ⁃ ｓｏｎｉｎｇ， ２００３， ３１（１）： １１⁃２１． ［８］ＤＡＶＩＳ Ｍ， ＰＵＴＮＡＭ Ｈ． Ａ ｃｏｍｐｕｔｉｎｇ ｐｒｏｃｅｄｕｒｅ ｆｏｒ ｑｕａｎｔｉ⁃ ｆｉｃａｔｉｏｎ ｔｈｅｏｒｙ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ ｔｈｅ ＡＣＭ， １９６０， ７（３）： ２０１⁃ ２１５． ［９］ ＤＡＶＩＳ Ｍ， ＬＯＧＥＭＡＮＮ Ｇ， ＬＯＶＥＬＡＮＤ Ｄ． Ａ ｍａｃｈｉｎｅ ｐｒｏｇｒａｍ ｆｏｒ ｔｈｅｏｒｅｍ⁃ｐｒｏｖｉｎｇ［Ｊ］． Ｃｏｍｍｕｎｉｃａｔｉｏｎｓ ｏｆ ｔｈｅ ＡＣＭ， １９６２， ５（７）： ３９４⁃３９７． ［１０］赖永，欧阳丹彤，蔡敦波，等．基于扩展规则的模型计数 与智能规划方 法［Ｊ］． 计算机研究与发展， ２００９， ４６ （３）： ４５９⁃４６９． ＬＡＩ Ｙｏｎｇ， ＯＵＹＡＮＧ Ｄａｎｔｏｎｇ， ＣＡＩ Ｄｕｎｂｏ， ｅｔ ａｌ． Ｍｏｄｅｌ ｃｏｕｎｔｉｎｇ ａｎｄ ｐｌａｎｎｉｎｇ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｒｅｓｅａｒｃｈ ａｎｄ Ｄｅｖｅｌｏｐｍｅｎｔ， ２００９， ４６（３）： ４５９⁃ ４６９． ［１１］ ＳＡＮＧ Ｔ， ＢＥＡＭＥ Ｐ， ＫＡＵＴＺ Ｈ． Ｓｏｌｖｉｎｇ Ｂａｙｅｓｉａｎ ｎｅｔ⁃ ｗｏｒｋｓ ｂｙ ｗｅｉｇｈｔｅｄ ｍｏｄｅｌ ｃｏｕｎｔｉｎｇ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ Ｔｗｅｎｔｉｅｔｈ Ｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ． Ｐｉｔｔｓｂｕｒｇｈ， ＵＳＡ， ２００５： ４７５⁃４８２． ［１２］谷文祥，李淑霞，殷明浩．隐蔽集的研究及发展［ Ｊ］．计算 机科学， ２０１０， ３７（３）： １１⁃１６． ＧＵ Ｗｅｎｘｉａｎｇ， ＬＩ Ｓｈｕｘｉａ， ＹＩＮ Ｍｉｎｇｈａｏ． Ｒｅｓｅａｒｃｈ ａｎｄ ｄｅ⁃ ｖｅｌｏｐｍｅｎｔ ｉｎ ｂａｃｋｄｏｏｒ ｓｅｔ［ Ｊ］． Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， ２０１０， ３７（３）： １１⁃１６． ［１３］ＮＩＳＨＩＭＵＲＡ Ｎ， ＲＡＧＤＥ Ｐ， ＳＺＥＩＤＥＲ Ｓ． Ｄｅｔｅｃｔｉｎｇ ｂａｃｋ⁃ ｄｏｏｒ ｓｅｔｓ ｗｉｔｈ ｒｅｓｐｅｃｔ ｔｏ Ｈｏｒｎ ａｎｄ ｂｉｎａｒｙ ｃｌａｕｓｅｓ ［ Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ７ｔｈ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｔｈｅｏｒｙ ａｎｄ Ａｐｐｌｉｃａｔｉｏｎｓ ｏｆ Ｓａｔｉｓｆｉａｂｉｌｉｔｙ Ｔｅｓｔｉｎｇ． Ｖａｎｃｏｕｖｅｒ， Ｃａｎ⁃ ａｄａ， ２００４： ９６⁃１０３． ［１４］ＭＮＡＳＳＯＮ Ｎ， ＺＥＣＣＨＩＮＡ Ｒ， ＫＩＲＫＰＡＴＲＩＣＫ Ｓ． Ｄｅｔｅｒ⁃ ｍｉｎｉｎｇ ｃｏｍｐｕｔａｔｉｏｎａｌ ｃｏｍｐｌｅｘｉｔｙ ｆｏｒｍ ｃｈａｒａｃｔｅｒｉｓｔｉｃ ‘ｐｈａｓｅ ｔｒａｎｓｉｔｉｏｎｓ’［Ｊ］． Ｎａｔｕｒｅ， １９９９， ４００： １３３⁃１３７． ［１５］林海．基于扩展规则的定理证明和知识编译［Ｄ］．长春： 吉林大学， ２００３： １⁃４０． ＬＩＮ Ｈａｉ． Ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ａｎｄ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｂａｓｅｄ ｏｎ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ［Ｄ］． Ｃｈａｎｇｃｈｕｎ： Ｊｉｌｉｎ Ｕｎｉｖｅｒ⁃ ｓｉｔｙ， ２００３： １⁃４０． ［１６］ＷＵ Ｘｉａ， ＳＵＮ Ｊｉｇｕｉ， ＬＵ Ｓｈｕａｉ， ｅｔ ａｌ． Ｉｍｐｒｏｖｅｄ ｐｒｏｐｏｓｉ⁃ ｔｉｏｎａｌ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ Ｆｉｒｓｔ Ｉｎｔｅｒｎａ⁃ ｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｒｏｕｇｈ Ｓｅｔｓ ａｎｄ Ｋｎｏｗｌｅｄｇｅ Ｔｅｃｈｎｏｌｏ⁃ ｇｙ． Ｃｈｏｎｇｑｉｎｇ， Ｃｈｉｎａ， ２００６： ５９２⁃５９７． 第 １ 期 王金艳，等：扩展规则方法研究综述 ·９·

10· 智能系统学报 第9卷 [17]吴瑕.基于扩展规则的定理证明的研究[D]长春：吉林 GU Wenxiang,ZHAO Xiaowei,YIN Minghao.Knowledge 大学，2006：1-132. compilation survey[J].Computer Science,2010,37(7): WU Xia.The research on the extension rule based theorem 20-26. proving[D].Changchun:Jilin University,2006:1-132. [28 MURRAY N V,ROSENTHAL E.Duality in knowledge [18]李莹，孙吉贵，吴瑕，等.基于MOM和BOHM启发式策 compilation techniques[C]//Proceedings of the 15th In- 略的扩展规则算法[J].软件学报，2009,20(6)：1521- ternational Symposium on Foundations of Intelligent Sys- 1527. tems.Saratoga Springs,USA,2005:182-190. LI Ying,SUN Jigui,WU Xia,et al.Extension rule algo- [29]谷文祥，王金艳，殷明浩.基于MCN和M0启发式策略 rithms based on IMOM and IBOHM heuristics strategies 的扩展规则知识编译方法[J].计算机研究与发展， [J].Journal of Software,2009,20(6):1521-1527. 2011,48(11):2064-2073. [19]WU Xia,SUN Jigui,LU Shuai,et al.Propositional exten- GU Wenxiang,WANG Jinyan,YIN Minghao.Knowledge sion rule with reduction[J].International Journal of Com- compilation using extension rule based on MCN and MO puter Science and Network Security,2006,6(1A):190- heuristic strategies[].Journal of Computer Research and 197. Development.2011,48(11):2064-2073. [20]孙吉贵，李莹，朱兴军，等.一种新的基于扩展规则的定 [30]赖永.基于ECCL理论的知识编译方法[D].长春：吉林 理证明算法[J].计算机研究与发展，2009,46(1)：9 大学，2010：146. 14. LAI Yong.Research on the knowledge compilation method SUN Jigui,LI Ying,ZHU Xingjun,et al.A novel theorem based on the EPCCL theory[D].Changchun:Jilin Univer- proving algorithm based on extension rule[J].Journal of 8ity,2010:1-46. Computer Research and Development,2009,46(1):9- [31]刘大有，赖永，林海.C2E:一个高性能的EPCCL编译器 14. [J].计算机学报，2013,36(6)：1254-1260. [21]张立明，欧阳丹形，白洪涛.基于半扩展规则的定理证明 LIU Dayou,LAI Yong,LIN Hai.C2E:an EPCCL compil- 方法[J].计算机研究与发展，2010,49(7)：1522-1529 er with good performance[J].Chinese Journal of Comput- ZHANG Liming,OUYANG Dangtong,BAI Hongtao.The- e8,2013,36(6):1254-1260. orem proving algorithm based on semi-extension rule[J]. [32]YIN Minghao,LIN Hai,SUN Jigui.Counting models using Journal of Computer Research and Development,2010,49 extension rules [C]//Proceedings of the Twenty-Second (7):1522-1529. National Conference on Artificial Intelligence.Vancouver, [22]ZHANG Liming,OUYANG Dantong,ZHAO Jian,et al. Canada,2007:1916-1917. The parallel theorem proving algorithm based on semi-ex- [33]殷明浩，林海，孙吉贵.一种基于扩展规则的#SAT求解 tension rule[]].Applied Mathematics Information Sci- 系统[J].软件学报，2009,20(7)：1714-1725 ences,2012,6(1):119-122. YIN Minghao,LIN Hai,SUN Jigui.Solving #SAT using [23 YIN Liangze,HE Fei,HUNG W NN,et al.Maxterm cov- extension rules J].Journal of Software,2009,20(7): ering for satisfiability[J].IEEE Transactions on Comput- 1714-1725. es,2012,61(3):420-426. [34]BIRNBAUM E,LOZINSKII E.The good old Davis-Putnam [24]XU Youjun,OUYANG Dantong,YE Yuxin,et al.Solving procedure helps counting models[J].Journal of Artificial SAT problem with a revised hitting set algorithm[C]//Pro- Intelligence Research,1999,10:457-477. ceedings of the 2nd International Conference on Future [35]BACCHUS F,DALMAO S,PITASSI T.Algorithms and Computer and Communication.Wuhan,China,2010:653- complexity results for #SAT and Bayesian inference[C]// 656. Proceedings of the 44th Symposium on Foundations of [25]许有军.基于扩展规则的若干SAT问题研究[D].长春： Computer Science.Cambridge,USA,2003:340-351. 吉林大学，2011：191. [36]许有军，欧阳丹彤，叶育鑫，等.间接使用扩展规则求解# XU Youjun.Research on several SAT issues based on ex- SAT问题[J].吉林大学学报：工学版，2011,41(4)： tension rule[D].Changchun:Jilin University,2011:1- 1047-1053 91. XU Youjun,OUYANG Dantong,YE Yuxin,et al.Solving [26]LIN Hai,SUN Jigui.Knowledge compilation using the ex- #SAT with extension rule indirectly[J].Journal of Jilin U. tension rule[J].Journal of Automated Reasoning,2004, niversity:Engineering and Technology Edition,2011,41 32(2):93-102. (4):1047-1053. 「271谷文祥，赵晓威，殷明浩.知识编译研究「J].计算机科 [37]HOOKER J N,RAGO G,CHANDRU V,et al.Partial in- 学，2010,37(7)：20-26. stantiation methods for inference in first-order logic [J]

［１７］吴瑕．基于扩展规则的定理证明的研究［Ｄ］．长春：吉林 大学， ２００６： １⁃１３２． ＷＵ Ｘｉａ． Ｔｈｅ ｒｅｓｅａｒｃｈ ｏｎ ｔｈｅ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｂａｓｅｄ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ［Ｄ］． Ｃｈａｎｇｃｈｕｎ： Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， ２００６： １⁃１３２． ［１８］李莹，孙吉贵，吴瑕，等．基于 ＩＭＯＭ 和 ＩＢＯＨＭ 启发式策 略的扩展规则算法［Ｊ］．软件学报， ２００９， ２０（６）： １５２１⁃ １５２７． ＬＩ Ｙｉｎｇ， ＳＵＮ Ｊｉｇｕｉ， ＷＵ Ｘｉａ， ｅｔ ａｌ． Ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ａｌｇｏ⁃ ｒｉｔｈｍｓ ｂａｓｅｄ ｏｎ ＩＭＯＭ ａｎｄ ＩＢＯＨＭ ｈｅｕｒｉｓｔｉｃｓ ｓｔｒａｔｅｇｉｅｓ ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔｗａｒｅ， ２００９， ２０（６）： １５２１⁃１５２７． ［１９］ＷＵ Ｘｉａ， ＳＵＮ Ｊｉｇｕｉ， ＬＵ Ｓｈｕａｉ， ｅｔ ａｌ． Ｐｒｏｐｏｓｉｔｉｏｎａｌ ｅｘｔｅｎ⁃ ｓｉｏｎ ｒｕｌｅ ｗｉｔｈ ｒｅｄｕｃｔｉｏｎ［ Ｊ］． Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍ⁃ ｐｕｔｅｒ Ｓｃｉｅｎｃｅ ａｎｄ Ｎｅｔｗｏｒｋ Ｓｅｃｕｒｉｔｙ， ２００６， ６（１Ａ）： １９０⁃ １９７． ［２０］孙吉贵，李莹，朱兴军，等．一种新的基于扩展规则的定 理证明算法［Ｊ］．计算机研究与发展， ２００９， ４６（１）： ９⁃ １４． ＳＵＮ Ｊｉｇｕｉ， ＬＩ Ｙｉｎｇ， ＺＨＵ Ｘｉｎｇｊｕｎ， ｅｔ ａｌ． Ａ ｎｏｖｅｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ａｌｇｏｒｉｔｈｍ ｂａｓｅｄ ｏｎ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｒｅｓｅａｒｃｈ ａｎｄ Ｄｅｖｅｌｏｐｍｅｎｔ， ２００９， ４６ （ １）： ９⁃ １４． ［２１］张立明，欧阳丹彤，白洪涛．基于半扩展规则的定理证明 方法［Ｊ］．计算机研究与发展， ２０１０， ４９（７）： １５２２⁃１５２９． ＺＨＡＮＧ Ｌｉｍｉｎｇ， ＯＵＹＡＮＧ Ｄａｎｇｔｏｎｇ， ＢＡＩ Ｈｏｎｇｔａｏ． Ｔｈｅ⁃ ｏｒｅｍ ｐｒｏｖｉｎｇ ａｌｇｏｒｉｔｈｍ ｂａｓｅｄ ｏｎ ｓｅｍｉ⁃ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｒｅｓｅａｒｃｈ ａｎｄ Ｄｅｖｅｌｏｐｍｅｎｔ， ２０１０， ４９ （７）： １５２２⁃１５２９． ［２２］ ＺＨＡＮＧ Ｌｉｍｉｎｇ， ＯＵＹＡＮＧ Ｄａｎｔｏｎｇ， ＺＨＡＯ Ｊｉａｎ， ｅｔ ａｌ． Ｔｈｅ ｐａｒａｌｌｅｌ ｔｈｅｏｒｅｍ ｐｒｏｖｉｎｇ ａｌｇｏｒｉｔｈｍ ｂａｓｅｄ ｏｎ ｓｅｍｉ⁃ｅｘ⁃ ｔｅｎｓｉｏｎ ｒｕｌｅ［ Ｊ］． Ａｐｐｌｉｅｄ Ｍａｔｈｅｍａｔｉｃｓ ＆ Ｉｎｆｏｒｍａｔｉｏｎ Ｓｃｉ⁃ ｅｎｃｅｓ， ２０１２， ６（１）： １１９⁃１２２． ［２３］ＹＩＮ Ｌｉａｎｇｚｅ， ＨＥ Ｆｅｉ， ＨＵＮＧ Ｗ Ｎ Ｎ， ｅｔ ａｌ． Ｍａｘｔｅｒｍ ｃｏｖ⁃ ｅｒｉｎｇ ｆｏｒ ｓａｔｉｓｆｉａｂｉｌｉｔｙ［ Ｊ］． ＩＥＥＥ Ｔｒａｎｓａｃｔｉｏｎｓ ｏｎ Ｃｏｍｐｕｔ⁃ ｅｒｓ， ２０１２， ６１（３）： ４２０⁃４２６． ［２４］ＸＵ Ｙｏｕｊｕｎ， ＯＵＹＡＮＧ Ｄａｎｔｏｎｇ， ＹＥ Ｙｕｘｉｎ， ｅｔ ａｌ． Ｓｏｌｖｉｎｇ ＳＡＴ ｐｒｏｂｌｅｍ ｗｉｔｈ ａ ｒｅｖｉｓｅｄ ｈｉｔｔｉｎｇ ｓｅｔ ａｌｇｏｒｉｔｈｍ［Ｃ］ ／ ／ Ｐｒｏ⁃ ｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ｆｕｔｕｒｅ Ｃｏｍｐｕｔｅｒ ａｎｄ Ｃｏｍｍｕｎｉｃａｔｉｏｎ． Ｗｕｈａｎ， Ｃｈｉｎａ， ２０１０： ６５３⁃ ６５６． ［２５］许有军．基于扩展规则的若干 ＳＡＴ 问题研究［Ｄ］．长春： 吉林大学， ２０１１： １⁃９１． ＸＵ Ｙｏｕｊｕｎ． Ｒｅｓｅａｒｃｈ ｏｎ ｓｅｖｅｒａｌ ＳＡＴ ｉｓｓｕｅｓ ｂａｓｅｄ ｏｎ ｅｘ⁃ ｔｅｎｓｉｏｎ ｒｕｌｅ［ Ｄ］． Ｃｈａｎｇｃｈｕｎ： Ｊｉｌｉｎ Ｕｎｉｖｅｒｓｉｔｙ， ２０１１： １⁃ ９１． ［２６］ＬＩＮ Ｈａｉ， ＳＵＮ Ｊｉｇｕｉ． Ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｕｓｉｎｇ ｔｈｅ ｅｘ⁃ ｔｅｎｓｉｏｎ ｒｕｌｅ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ａｕｔｏｍａｔｅｄ Ｒｅａｓｏｎｉｎｇ， ２００４， ３２（２）： ９３⁃１０２． ［２７］谷文祥，赵晓威，殷明浩．知识编译研究［ Ｊ］．计算机科 学， ２０１０， ３７（７）： ２０⁃２６． ＧＵ Ｗｅｎｘｉａｎｇ， ＺＨＡＯ Ｘｉａｏｗｅｉ， ＹＩＮ Ｍｉｎｇｈａｏ． Ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｓｕｒｖｅｙ［Ｊ］． Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ， ２０１０， ３７（７）： ２０⁃２６． ［２８］ ＭＵＲＲＡＹ Ｎ Ｖ， ＲＯＳＥＮＴＨＡＬ Ｅ． Ｄｕａｌｉｔｙ ｉｎ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｔｅｃｈｎｉｑｕｅｓ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ １５ｔｈ Ｉｎ⁃ ｔｅｒｎａｔｉｏｎａｌ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｆｏｕｎｄａｔｉｏｎｓ ｏｆ Ｉｎｔｅｌｌｉｇｅｎｔ Ｓｙｓ⁃ ｔｅｍｓ． Ｓａｒａｔｏｇａ Ｓｐｒｉｎｇｓ， ＵＳＡ， ２００５： １８２⁃１９０． ［２９］谷文祥，王金艳，殷明浩．基于 ＭＣＮ 和 ＭＯ 启发式策略 的扩展规则知识编译方法［ Ｊ］． 计算机研究与发展， ２０１１， ４８（１１）： ２０６４⁃２０７３． ＧＵ Ｗｅｎｘｉａｎｇ， ＷＡＮＧ Ｊｉｎｙａｎ， ＹＩＮ Ｍｉｎｇｈａｏ． Ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｂａｓｅｄ ｏｎ ＭＣＮ ａｎｄ ＭＯ ｈｅｕｒｉｓｔｉｃ ｓｔｒａｔｅｇｉｅｓ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔｅｒ Ｒｅｓｅａｒｃｈ ａｎｄ Ｄｅｖｅｌｏｐｍｅｎｔ， ２０１１， ４８（１１）： ２０６４⁃２０７３． ［３０］赖永．基于 ＥＰＣＣＬ 理论的知识编译方法［Ｄ］．长春：吉林 大学， ２０１０： １⁃４６． ＬＡＩ Ｙｏｎｇ． Ｒｅｓｅａｒｃｈ ｏｎ ｔｈｅ ｋｎｏｗｌｅｄｇｅ ｃｏｍｐｉｌａｔｉｏｎ ｍｅｔｈｏｄ ｂａｓｅｄ ｏｎ ｔｈｅ ＥＰＣＣＬ ｔｈｅｏｒｙ［Ｄ］． Ｃｈａｎｇｃｈｕｎ： Ｊｉｌｉｎ Ｕｎｉｖｅｒ⁃ ｓｉｔｙ， ２０１０： １⁃４６． ［３１］刘大有，赖永，林海．Ｃ２Ｅ：一个高性能的 ＥＰＣＣＬ 编译器 ［Ｊ］．计算机学报， ２０１３， ３６（６）： １２５４⁃１２６０． ＬＩＵ Ｄａｙｏｕ， ＬＡＩ Ｙｏｎｇ， ＬＩＮ Ｈａｉ． Ｃ２Ｅ： ａｎ ＥＰＣＣＬ ｃｏｍｐｉｌ⁃ ｅｒ ｗｉｔｈ ｇｏｏｄ ｐｅｒｆｏｒｍａｎｃｅ［ Ｊ］． Ｃｈｉｎｅｓｅ Ｊｏｕｒｎａｌ ｏｆ Ｃｏｍｐｕｔ⁃ ｅｒｓ， ２０１３， ３６（６）： １２５４⁃１２６０． ［３２］ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩＮ Ｈａｉ， ＳＵＮ Ｊｉｇｕｉ． Ｃｏｕｎｔｉｎｇ ｍｏｄｅｌｓ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅｓ ［ Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ Ｔｗｅｎｔｙ⁃Ｓｅｃｏｎｄ Ｎａｔｉｏｎａｌ Ｃｏｎｆｅｒｅｎｃｅ ｏｎ Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ． Ｖａｎｃｏｕｖｅｒ， Ｃａｎａｄａ， ２００７： １９１６⁃１９１７． ［３３］殷明浩，林海，孙吉贵．一种基于扩展规则的＃ＳＡＴ 求解 系统［Ｊ］．软件学报， ２００９， ２０（７）： １７１４⁃１７２５． ＹＩＮ Ｍｉｎｇｈａｏ， ＬＩＮ Ｈａｉ， ＳＵＮ Ｊｉｇｕｉ． Ｓｏｌｖｉｎｇ ＃ＳＡＴ ｕｓｉｎｇ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅｓ ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｓｏｆｔｗａｒｅ， ２００９， ２０ （ ７）： １７１４⁃１７２５． ［３４］ＢＩＲＮＢＡＵＭ Ｅ， ＬＯＺＩＮＳＫＩＩ Ｅ． Ｔｈｅ ｇｏｏｄ ｏｌｄ Ｄａｖｉｓ⁃Ｐｕｔｎａｍ ｐｒｏｃｅｄｕｒｅ ｈｅｌｐｓ ｃｏｕｎｔｉｎｇ ｍｏｄｅｌｓ［ Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ａｒｔｉｆｉｃｉａｌ Ｉｎｔｅｌｌｉｇｅｎｃｅ Ｒｅｓｅａｒｃｈ， １９９９， １０： ４５７⁃４７７． ［３５］ ＢＡＣＣＨＵＳ Ｆ， ＤＡＬＭＡＯ Ｓ， ＰＩＴＡＳＳＩ Ｔ． Ａｌｇｏｒｉｔｈｍｓ ａｎｄ ｃｏｍｐｌｅｘｉｔｙ ｒｅｓｕｌｔｓ ｆｏｒ ＃ＳＡＴ ａｎｄ Ｂａｙｅｓｉａｎ ｉｎｆｅｒｅｎｃｅ［Ｃ］ ／ ／ Ｐｒｏｃｅｅｄｉｎｇｓ ｏｆ ｔｈｅ ４４ｔｈ Ｓｙｍｐｏｓｉｕｍ ｏｎ Ｆｏｕｎｄａｔｉｏｎｓ ｏｆ Ｃｏｍｐｕｔｅｒ Ｓｃｉｅｎｃｅ． Ｃａｍｂｒｉｄｇｅ， ＵＳＡ， ２００３： ３４０⁃３５１． ［３６］许有军，欧阳丹彤，叶育鑫，等．间接使用扩展规则求解＃ ＳＡＴ 问题［ Ｊ］．吉林大学学报：工学版， ２０１１， ４１ （ ４）： １０４７⁃１０５３． ＸＵ Ｙｏｕｊｕｎ， ＯＵＹＡＮＧ Ｄａｎｔｏｎｇ， ＹＥ Ｙｕｘｉｎ， ｅｔ ａｌ． Ｓｏｌｖｉｎｇ ＃ＳＡＴ ｗｉｔｈ ｅｘｔｅｎｓｉｏｎ ｒｕｌｅ ｉｎｄｉｒｅｃｔｌｙ［Ｊ］． Ｊｏｕｒｎａｌ ｏｆ Ｊｉｌｉｎ Ｕ⁃ ｎｉｖｅｒｓｉｔｙ： Ｅｎｇｉｎｅｅｒｉｎｇ ａｎｄ Ｔｅｃｈｎｏｌｏｇｙ Ｅｄｉｔｉｏｎ， ２０１１， ４１ （４）： １０４７⁃１０５３． ［３７］ＨＯＯＫＥＲ Ｊ Ｎ， ＲＡＧＯ Ｇ， ＣＨＡＮＤＲＵ Ｖ， ｅｔ ａｌ． Ｐａｒｔｉａｌ ｉｎ⁃ ｓｔａｎｔｉａｔｉｏｎ ｍｅｔｈｏｄｓ ｆｏｒ ｉｎｆｅｒｅｎｃｅ ｉｎ ｆｉｒｓｔ⁃ｏｒｄｅｒ ｌｏｇｉｃ ［ Ｊ］． ·１０· 智 能 系 统 学 报 第 ９ 卷