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