基于扩展规则的模型计数与智能规划方法  

Model Counting and Planning Using Extension Rule

作　　者：赖永[1,2] 欧阳丹彤[1,2] 蔡敦波[1,2] 吕帅[1,2] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]吉林大学符号计算与知识工程教育部重点实验室,长春130012

出　　处：《计算机研究与发展》2009年第3期459-469,共11页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(607730097);教育部高等学校博士学科点专项科研基金项目(20050183065)~~

摘　　要：提出命题扩展规则方法ER的一种高效实现.在此基础上,研究了扩展规则方法在3个领域的应用:提出一次性求解一系列相近SAT问题的快速算法nER;提出基于扩展规则的模型计数算法#ER,同时结合#ER和#DPLL的优点提出算法#CDE;设计基于扩展规则方法的Conformant规划系统.实验结果表明:使用nER算法一次性求解的时间远小于使用ER方法单独求解每个问题的总时间;对于互补因子较高的问题,#ER优于#DPLL;#CDE融合了#ER和#DPLL的优点.研究表明扩展规则方法对于互补因子较高的问题具有较大的优势,具有广阔的应用前景.Methods based on extension rule are new approaches for automated theorem proving and can efficiently solve problems with high complementary factor. In this paper, a new strategy to reimplement ER, which is an algorithm based on the propositional extension rule, is proposed. The new implementation of ER is superior to the original one. Based on this, the extension rule is applied in the following three areas. Firstly, there exist a set of analogous SAT problems being solved in real applications. In contrast with solving these SAT problems separately, an algorithm called nER that solves them as a whole is developed. The algorithm hER exploits the repetition property of ER and generally costs less time than the total time of using ER to solve every problem. Furthermore, based on ER, two new algorithms called #ER and #CDE are proposed, the latter being a combination of #ER and #DPLL. Experimental results show that #ER outperforms #DPLL on a wide range of problems and the #CDE integrates advantages of #ER and #DPLL. Finally, an ER based SAT solver is embedded into the conformant fast-forward to study the potential of ER based methods in artificial intelligence planning. Preliminary results show the e＇fficiency of ER and future research topics.

关 键 词：自动推理 扩展规则 命题可满足问题 模型计数 Conformant规划 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]