文章快速检索 高级检索

1. 广西师范大学 计算机科学与信息工程学院，广西 桂林 541004;
2. 长春建筑学院 基础教学部，吉林 长春 130607;
3. 东北师范大学 计算机科学与信息技术学院，吉林 长春 130117

Extension rule: a survey
WANG Jinyan1 , GU Wenxiang2,3 , QIN Shaohua1 , YIN Minghao3
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 Science 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 resolution principle. In recent years, the method has received wide attention and has achieved great progress. This paper surveys the development of the theorem proving using the extension rule for ten years from three aspects: the related 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.
Key words: automated reasoning     resolution principle     extension rule     SAT     #SAT

1 相关概念

xM中的任意变量。

#SAT问题可以看作是加权模型计数问题的特例，其中每个文字的权值为0.5。

2 命题逻辑中的扩展规则求解方法

2.1 基于扩展规则的SAT求解方法

2.1.1 ER和IER算法

2003年，Lin等[7]沿着归结原理的反向提出一条新的推理规则—扩展规则，使用扩展规则进行定理证明的算法ER(theorem proving based on extension rule)，其基本思想是把给定的子句集Σ扩展成由极大项组成的子句集Σ′，然后根据极大项的个数|Σ′|来判定Σ的可满足性，如果|Σ′|=2m(mΣ的变量数)，则Σ是不可满足的；否则Σ可满足。事实上并不需要将Σ′扩展出来，只需计算出|Σ′|就可以判定Σ的可满足性。因此他们利用容斥原理直接计算出|Σ′|，降低了该方法的空间复杂性。一般情况下，ER算法的时间复杂性是指数级的，效率比较低，但是在任意2个子句都含有互补对的情况下，ER算法的效率较高，而使用基于归结的方法效率较低。可以用互补因子CF来比较基于扩展规则的方法和基于归结的方法。假设所有的SAT问题都在一个光谱上，其左端是互补因子为1的问题，其右端是互补因子为0的问题，在光谱左端用基于扩展规则的方法效率更高，而在光谱右端基于归结的方法效率更高。

ER算法实际上是在给定子句集的所有极大项组成的空间中进行搜索，看是否有不能被扩展出的极大项。为了减少搜索空间提高求解的效率，Lin等[7, 15]提出了一种高效的算法IER(improved extension rule)。该方法首先在极大项空间的一个子空间中搜索，如果在子空间中有不能被扩展的极大项，那么整个空间就有不能被扩展的极大项，这时子句集是可满足的；否则，不能判定子句集的可满足性，需要调用ER算法。IER算法是先运行一个高效但不完备的算法，希望它能解决大部分问题，对于无法解决的问题再调用完备的ER算法。

2.1.2 带化简规则的ER和IER算法

2.1.3 基于启发式策略的IER算法

IER算法通过随机选取子句C来限定极大项搜索空间，为了尽可能地在该子空间中判定出给定子句集的可满足性，以提高算法的效率，子句C的选取至关重要。Lin等在文献[7]中指出，对于具体的问题，通过问题的背景知识来调整子句C的输入可能会提高IER算法的效率，并将C的选取作为一个开放问题。

2.1.4 与归结方法的结合

2.1.5 避开容斥原理的扩展规则方法

1)子句集合包含方法。

2009年，孙吉贵等[20]发现一个极大项能被子句集扩展出来，子句集中必须有子句包含于该极大项(子句看作文字集合)。基于该性质，孙吉贵等提出了一种新的基于扩展规则的定理证明方法NER，该方法将SAT问题转化为一系列文字集合的包含问题。NER算法按照一定次序判断极大项是否可被当前待判定的子句集Σ扩展，若存在某个极大项不能被扩展出来, 那么Σ是可满足的；否则，若所有极大项都可以被扩展出来，则Σ是不可满足的。其最优和最坏时间复杂度分别为O(m+n×k2)和O(2m×(m+n×k2))，mnk分别表示子句集中变量的个数、子句的个数和子句的平均长度。实验结果表明，无论是对于随机问题还是标准测试用例，NER算法的执行效率较IER和DR算法都有很大的提高，有些问题可以提高2个数量级。

NER算法将所有极大项按照一定顺序来一一判定其是否能由子句集扩展出来，直到某个极大项不能被扩展时或者所有极大项都可由子句集扩展出来时，才能判定出子句集的可满足性。事实上，当一个极大项可由某一子句扩展时，接下来的部分极大项可以不用判断其是否可由子句集扩展出来，从而减少了需要判断的极大项个数。张立明等[21]定义了半扩展规则，并且提出了基于半扩展规则的定理证明方法SRE(semi-extension rule)。SRE算法是在NER算法的基础上，按一定顺序判定极大项是否可被子句集扩展，当一个极大项可被子句集中的某一子句扩展时，那么基于此子句半扩展出的所有极大项都不需判断其是否可被子句集扩展，这样减少了需要判断的极大项个数，使计算复杂度由原来NER方法的O(2m×(m+n×k2))降为O(2d×(m+n×k2)+n2)，其中d为子句集中子句的度的平均值。d越小，SRE算法的求解效率越高；当d趋近与m时，SRE算法的求解效率较NER算法提高较小。

2)极大项覆盖方法。

 图 1 C关于Σ的相对极大项 Fig. 1 The relative maxterm of C with respect to Σ

 图 2 一个可满足问题实例 Fig. 2 A satisfiable example

MC方法利用空子句关于子句集的相对极大项的个数来判定子句集的可满足性。如果相对极大项个数为0，则子句集是不可满足的；否则，子句集是可满足的。与扩展规则方法根据扩展出的极大项个数来判断子句集的可满足性不同，该方法直接计算出不能由子句集扩展出来的相对极大项个数，然后根据相对极大项个数来判断子句集的可满足性，避开了容斥原理的复杂性。进一步，他们在基本MC算法的基础上提出了8种优化策略，极大地提高了算法的求解效率。

3)碰集方法。

Xu等[24-25]找出了不能被扩展出的极大项具有的特征，以此来回避容斥原理所带来的计算量。他们发现，若极大项与子句集Σ中的某个子句互补，则该极大项不能由这个子句扩展出来。进而可知，如果极大项与Σ中所有子句都互补，那么该极大项就不能由Σ扩展出来。假定存在与Σ中任意子句都互补的极大项CM，那么由CM可以构造极大项CM′，其中CM′由CM中每个文字的补文字构成。如果将子句看作文字集合，Σ看作文字集合簇，那么CM′与Σ中任意子句的交都不为空，即CM′是Σ的碰集。基于此，Xu等证明了子句集是可满足的, 当且仅当该子句集存在不包含互补文字的碰集，这样就将SAT问题转化成判定是否存在不含互补文字的碰集问题，并且提出了2种有效的方法CBHST(complementary binary hitting set tree)和RNHST(revised new hitting set tree)来进行求解。这2种算法与DR相比，在效率方面都有1~2个数量级的提高。RNHST算法与CBHST算法相比，RNHST更适合长子句的情况，而CBHST更适合短子句的情况。

2.1.6 基于扩展规则的知识编译方法

1)基于KCER的知识编译方法。

Lin和Sun[26]指出扩展规则方法可以被应用于知识编译[27]中，他们定义了EPCCL(each pair contains complementary literal)理论(任意2个子句都含互补对子句集)，证明了EPCCL理论是在“可满足可控制类”和“蕴含可控制类”中，并证明对于任意子句集一定能找到一个与之等价的EPCCL理论，因此EPCCL理论可以作为知识编译的目标语言，进而利用“桶删除”的思想提出将给定子句集编译成EPCCL理论的算法KCER(knowledge compilation using the extension rule)。该方法与现有其他知识编译方法的不同之处在于：在编译阶段和推理阶段该方法都是基于扩展规则的，而其他的知识编译方法都是基于归结原理的；当互补因子较大的时候，该方法得到的子句集规模相对较小，特别地，当待编译的子句集本身就是一个EPCCL理论，用该方法编译后的结果就是其本身，而用其他方法编译，结果可能是指数级大的。因此，该方法被Murray教授看作是与现有其他知识编译方法对偶的一种方法[28]

2)基于启发式策略的知识编译方法。

3)新的EPCCL编译框架。

2.2 基于扩展规则的相近SAT求解方法

 (1)

2.3 基于扩展规则的#SAT求解方法

2.3.1 利用容斥原理的#SAT方法

2.3.2 避开容斥原理的#SAT方法

1)与归结方法的结合。

2)碰集方法。

3 扩展规则在其他逻辑中的应用

3.1 一阶逻辑

Wu等[38]指出Lin给出的原子被潜地阻塞的定义对新产生子句的条件限制过严，导致RPPI算法是不完备的，他们对潜在阻塞进行了重新定义，并且提出了一种新的一阶扩展规则算法RFOER(revised first-order extension rule)，该算法与RPPI算法主要有以下3点不同：1)RPPI算法不完备，而RFOER算法完备；2)RPPI调用的是基本的ER算法，而RFOER调用的是更为高效的带化简规则和启发式策略的ER算法；3)RFOER中增加了M-可满足的情形，使得算法可以被更灵活地应用，更适合用于求解实际的问题。

3.2 描述逻辑

3.3 模态逻辑

Wu等[42]利用破坏性方法直接把扩展规则方法推广到模态逻辑中，提出了模态系统K中的破坏性扩展规则方法DMKER(destructive extension rule in modal logic K)，该方法将利用化简规则进行简化和利用扩展规则判定不可满足性结合在一起，交替进行。DMKER算法能够快速地证明模态系统K中的所有公理和四类标准的benchmark问题。该方法继承了扩展规则方法的优点，当存在较多的互补公式时，模态逻辑推理的效率明显提高。此外，Wu等[43]分别将关系转换方法、函数转换方法与扩展规则方法相结合，提出了关系扩展规则方法MRER(modal relational extension rule)、连续模态逻辑中的函数扩展规则方法MFER(modal functional extension rule)和非连续模态逻辑的广义函数扩展规则方法GMFER(general modal functional extension rule)。

3.4 可能性逻辑

3.5 多值逻辑

4 待解决的问题

1)如何利用扩展规则方法求解隐蔽集。

2)如何选择IER算法的子句C使之与骨架集相对应。

3)探求扩展规则方法在其他逻辑中的应用。

5 结束语

 [1] 殷明浩.自动推理和智能规划中若干问题研究[D].长春:吉林大学, 2008: 1-109. YIN Minghao. The research on several issues of automated reasoning and artificial intelligent planning[D]. Changchun: Jilin University, 2008: 1-109. http://cdmd.cnki.com.cn/article/cdmd-10183-2008126532.htm [2] WOLFGANG R. The KIV system: systematic construction of verified software[C]//Proceedings of the 11th International Conference on Automated Deduction. Saratoga Springs, USA, 1992: 753-757. [3] 吕帅, 刘磊, 石莲, 等. 基于自动推理技术的智能规划方法[J]. 软件学报 , 2009, 20 (5) : 1226-1240 LU Shuai, LIU Lei, SHI Lian, et al. Artificial intelligence planning methods based on automated reasoning techniques[J]. Journal of Software , 2009, 20 (5) : 1226-1240 [4] GRASTIEN A, ANBULAGAN A, RINTANEN J, et al. Diagnosis of discrete-event systems using satisfiability algorithms[C]//Proceedings of the Twenty-Second Conference on Artificial Intelligence. Vancouver, Canada, 2007: 305-310. [5] ROBINSON J A. A machine oriented logic based on the resolution principle[J]. Computer Machine , 1965, 12 (1) : 23-41 DOI:10.1145/321250.321253 [6] DECHTER R, RISH I. Directional resolution: the Davis-Putnam procedure, revisited[C]//Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning. Bonn, Germany, 1994: 134-145. [7] LIN Hai, SUN Jigui, ZHANG Yimin. Theorem proving based on the extension rule[J]. Journal of Automated Reasoning , 2003, 31 (1) : 11-21 DOI:10.1023/A:1027339205632 [8] DAVIS M, PUTNAM H. A computing procedure for quantification theory[J]. Journal of the ACM , 1960, 7 (3) : 201-215 DOI:10.1145/321033.321034 [9] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem-proving[J]. Communications of the ACM , 1962, 5 (7) : 394-397 DOI:10.1145/368273.368557 [10] 赖永, 欧阳丹彤, 蔡敦波, 等. 基于扩展规则的模型计数与智能规划方法[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 networks 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 development in backdoor set[J]. Computer Science , 2010, 37 (3) : 11-16 [13] NISHIMURA N, RAGDE P, SZEIDER S. Detecting backdoor sets with respect to Horn and binary clauses[C]//Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing. Vancouver, Canada, 2004: 96-103. [14] MNASSON N, ZECCHINA R, KIRKPATRICK S. Determining computational complexity form characteristic 'phase transitions'[J]. Nature , 1999, 400 : 133-137 DOI:10.1038/22055 [15] 林海.基于扩展规则的定理证明和知识编译[D].长春:吉林大学, 2003: 1-40. LIN Hai. Theorem proving and knowledge compilation based on the extension rule[D]. Changchun: Jilin University, 2003: 1-40. http://d.wanfangdata.com.cn/Thesis/Y527971 [16] WU Xia, SUN Jigui, LU Shuai, et al. Improved propositional extension rule[C]//Proceedings of the First International Conference on Rough Sets and Knowledge Technology. Chongqing, China, 2006: 592-597. [17] 吴瑕.基于扩展规则的定理证明的研究[D].长春:吉林大学, 2006: 1-132. WU Xia. The research on the extension rule based theorem proving[D]. Changchun: Jilin University, 2006: 1-132. http://cdmd.cnki.com.cn/article/cdmd-10183-2006094302.htm [18] 李莹, 孙吉贵, 吴瑕, 等. 基于IMOM和IBOHM启发式策略的扩展规则算法[J]. 软件学报 , 2009, 20 (6) : 1521-1527 LI Ying, SUN Jigui, WU Xia, et al. Extension rule algorithms based on IMOM and IBOHM heuristics strategies[J]. Journal of Software , 2009, 20 (6) : 1521-1527 DOI:10.3724/SP.J.1001.2009.03420 [19] WU Xia, SUN Jigui, LU Shuai, et al. Propositional extension rule with reduction[J]. International Journal of Computer Science and Network Security , 2006, 6 (1A) : 190-197 [20] 孙吉贵, 李莹, 朱兴军, 等. 一种新的基于扩展规则的定理证明算法[J]. 计算机研究与发展 , 2009, 46 (1) : 9-14 SUN Jigui, LI Ying, ZHU Xingjun, et al. A novel theorem proving algorithm based on extension rule[J]. Journal of Computer Research and Development , 2009, 46 (1) : 9-14 [21] 张立明, 欧阳丹彤, 白洪涛. 基于半扩展规则的定理证明方法[J]. 计算机研究与发展 , 2010, 49 (7) : 1522-1529 ZHANG Liming, OUYANG Dangtong, BAI Hongtao. Theorem proving algorithm based on semi-extension rule[J]. Journal of Computer Research and Development , 2010, 49 (7) : 1522-1529 [22] ZHANG Liming, OUYANG Dantong, ZHAO Jian, et al. The parallel theorem proving algorithm based on semi-extension rule[J]. Applied Mathematics & Information Sciences , 2012, 6 (1) : 119-122 [23] YIN Liangze, HE Fei, HUNG W N N, et al. Maxterm covering for satisfiability[J]. IEEE Transactions on Computers , 2012, 61 (3) : 420-426 DOI:10.1109/TC.2010.270 [24] XU Youjun, OUYANG Dantong, YE Yuxin, et al. Solving SAT problem with a revised hitting set algorithm[C]//Proceedings of the 2nd International Conference on Future Computer and Communication. Wuhan, China, 2010: 653-656. [25] 许有军.基于扩展规则的若干SAT问题研究[D].长春:吉林大学, 2011: 1-91. XU Youjun. Research on several SAT issues based on extension rule[D]. Changchun: Jilin University, 2011: 1-91. http://cdmd.cnki.com.cn/Article/CDMD-10183-1011106010.htm [26] LIN Hai, SUN Jigui. Knowledge compilation using the extension rule[J]. Journal of Automated Reasoning , 2004, 32 (2) : 93-102 DOI:10.1023/B:JARS.0000029959.45572.44 [27] 谷文祥, 赵晓威, 殷明浩. 知识编译研究[J]. 计算机科学 , 2010, 37 (7) : 20-26 GU Wenxiang, ZHAO Xiaowei, YIN Minghao. Knowledge compilation survey[J]. Computer Science , 2010, 37 (7) : 20-26 [28] MURRAY N V, ROSENTHAL E. Duality in knowledge compilation techniques[C]//Proceedings of the 15th International Symposium on Foundations of Intelligent Systems. Saratoga Springs, USA, 2005: 182-190. [29] 谷文祥, 王金艳, 殷明浩. 基于MCN和MO启发式策略的扩展规则知识编译方法[J]. 计算机研究与发展 , 2011, 48 (11) : 2064-2073 GU Wenxiang, WANG Jinyan, YIN Minghao. Knowledge compilation using extension rule based on MCN and MO heuristic strategies[J]. Journal of Computer Research and Development , 2011, 48 (11) : 2064-2073 [30] 赖永.基于EPCCL理论的知识编译方法[D].长春:吉林大学, 2010: 1-46. LAI Yong. Research on the knowledge compilation method based on the EPCCL theory[D]. Changchun: Jilin University, 2010: 1-46. http://www.shangxueba.com/lunwen/v392830.html [31] 刘大有, 赖永, 林海. C2E:一个高性能的EPCCL编译器[J]. 计算机学报 , 2013, 36 (6) : 1254-1260 LIU Dayou, LAI Yong, LIN Hai. C2E: an EPCCL compiler with good performance[J]. Chinese Journal of Computers , 2013, 36 (6) : 1254-1260 [32] YIN Minghao, LIN Hai, SUN Jigui. Counting models using extension rules[C]//Proceedings of the Twenty-Second National Conference on Artificial Intelligence. Vancouver, Canada, 2007: 1916-1917. [33] 殷明浩, 林海, 孙吉贵. 一种基于扩展规则的#SAT求解系统[J]. 软件学报 , 2009, 20 (7) : 1714-1725 YIN Minghao, LIN Hai, SUN Jigui. Solving #SAT using extension rules[J]. Journal of Software , 2009, 20 (7) : 1714-1725 [34] BIRNBAUM E, LOZINSKII E. The good old Davis-Putnam procedure helps counting models[J]. Journal of Artificial Intelligence Research , 1999, 10 : 457-477 [35] BACCHUS F, DALMAO S, PITASSI T. Algorithms and complexity results for #SAT and Bayesian inference[C]//Proceedings of the 44th Symposium on Foundations of Computer Science. Cambridge, USA, 2003: 340-351. [36] 许有军, 欧阳丹彤, 叶育鑫, 等. 间接使用扩展规则求解#SAT问题[J]. 吉林大学学报:工学版 , 2011, 41 (4) : 1047-1053 XU Youjun, OUYANG Dantong, YE Yuxin, et al. Solving #SAT with extension rule indirectly[J]. Journal of Jilin University: Engineering and Technology Edition , 2011, 41 (4) : 1047-1053 [37] HOOKER J N, RAGO G, CHANDRU V, et al. Partial instantiation methods for inference in first-order logic[J]. Journal of Automated Reasoning , 2002, 28 (4) : 371-396 DOI:10.1023/A:1015854101244 [38] WU Xia, SUN Jigui, HOU Kun. Extension rule in first order logic[C]//Proceedings of the 5th International Conference on Cognitive Informatics. Beijing, China, 2006: 701-706. [39] BAADER F, CALVANESE D, MCGUINNESS D, et al. The description logic handbook: theory, implementation and applications[M]. New York: Cambridge University Press, 2003 . [40] ZOU Tingting, LIU Lei, LU Shuai. Knowledge compilation for description logic based on concept extension rule[J]. Journal of Computational Information System , 2012, 8 (6) : 2409-2416 [41] HALPERN J Y, MOSES Y. A guide to completeness and complexity for modal logics of knowledge and belief[J]. Artificial Intelligence , 1992, 54 (3) : 319-379 DOI:10.1016/0004-3702(92)90049-4 [42] WU Xia, SUN Jigui. Destructive extension rule in proposition modal logic K[M]//LIU G R, TAN V B C, HAN X. Computational Methods. Dordrecht, The Netherlands: Springer, 2006: 1087-1091. [43] WU Xia, SUN Jigui, LIN Hai, et al. Modal extension rule[J]. Progress in Natural Science , 2005, 15 (6) : 550-558 DOI:10.1080/10020070512331342540 [44] DUBOIS D, PRADE H. Possibilistic logic: a retrospective and prospective view[J]. Fuzzy Sets and Systems , 2004, 144 (1) : 3-23 DOI:10.1016/j.fss.2003.10.011 [45] 殷明浩, 孙吉贵, 林海, 等. 可能性扩展规则的推理和知识编译[J]. 软件学报 , 2010, 21 (11) : 2826-2837 YIN Minghao, SUN Jigui, LIN Hai, et al. Possibilistic extension rules for reasoning and knowledge compilation[J]. Journal of Software , 2010, 21 (11) : 2826-2837 [46] 谷文祥, 郭鸿鹤, 殷明浩, 等. 多值知识编译[J]. 东北师范大学学报:自然科学版 , 2011, 43 (4) : 44-48 GU Xenxiang, GUO Honghe, YIN Minghao, et al. Compiling multi-valued knowledge base[J]. Journal of Northeast Normal University: Natural Science Edition , 2011, 43 (4) : 44-48
DOI: 10.3969/j.issn.1673-4785.201308004

0

#### 文章信息

WANG Jinyan, GU Wenxiang, QIN Shaohua, YIN Minghao

Extension rule: a survey

CAAI Transactions on Intelligent Systems, 2014, 9(1): 1-11
http://dx.doi.org/10.3969/j.issn.1673-4785.201308004