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