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

Model Counting and Planning Using Extension Rule

提出命题扩展规则方法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.