刘磊, 牛当当, 李壮, 吕帅

(吉林大学 计算机科学与技术学院,吉林 长春130012)

基于超扩展规则的动态在线推理算法

刘磊, 牛当当, 李壮, 吕帅

(吉林大学 计算机科学与技术学院,吉林 长春130012)

摘要：为了提高扩展规则的扩展性能，提出了超扩展规则，并证明了其与扩展负超归结之间的关联关系。KCER算法中使用扩展规则扩展子句，利用超扩展规则替换扩展规则能够更清晰地展示扩展过程，因此提出了基于超扩展规则的动态在线推理算法IKCCER。IKCCER采用离线编译和在线推理过程交互执行的方式，在保持推理效率不变的同时，其空间复杂性为KCCER算法空间复杂性的2/(n+1)，其中n为输入子句集的子句数。

关键词：自动推理；知识编译；扩展规则；超扩展规则；动态在线推理

网络出版地址：http://www.cnki.net/kcms/detail/23.1390.U.20151104.1633.004.html

吕帅(1981-)，男，讲师.

许多约束问题仅判定是否可满足是远远不够的，如将概率推理问题[1]、一致性概率规划问题[2]转换为命题公式集后，除了判断可满足性，还需求解#SAT问题，即计算该公式集中的模型数。求解#SAT问题的方法通常可分为离线推理和知识编译后在线推理。

在离线推理的研究中，在扩展规则提出之前，绝大多数#SAT问题的求解算法都是基于#DPLL算法设计的[3]。林海等[4]提出了扩展规则推理方法(extension rule，ER)，被著名人工智能专家Davis称为与归结方法“互补”的方法。扩展规则推理方法通过计算输入子句集所能扩展出的极大项数来判断其可满足性及模型数。殷明浩等[5]基于容斥原理提出了解决ER算法空间复杂性问题的CER算法；……