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