ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2016, Vol. 53 ›› Issue (7): 1596-1604.doi: 10.7544/issn1000-1239.2016.20150032

• 人工智能 • 上一篇    下一篇



  1. (吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (
  • 出版日期: 2016-07-01
  • 基金资助: 

An Algorithm Based on Extension Rule For Solving #SAT Using Complementary Degree

Ouyang Dantong, Jia Fengyu, Liu Siguang, Zhang Liming   

  1. (College of Computer Science and Technology, Jilin University, Changchun 130012) (Key Laboratory of Symbolic Computation and Knowledge Engineering (Jilin University), Ministry of Education, Changchun 130012)
  • Online: 2016-07-01

摘要: #SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一,在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法CER(counting models using extension rules)深入研究的基础上,提出一种结合互补度的#SAT问题求解方法.在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合,并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备.提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数.实验结果表明:与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足.

关键词: 扩展规则, 模型计数, CER方法, 互补度, 集合枚举树

Abstract: The #SAT problem also called model counting is one of the important and challenging problems in artificial intelligence. It is used widely in the field of artificial intelligence. After doing the in-depth study of model counting algorithm CER that is based on Extension Rule, we propose a method using complementary degree for #SAT problem in this paper. We formalize the computing procedure of solving #SAT problem by introducing SE-Tree which produces all the subsets of clause set that need to be computed. As the closed nodes are added into the SE-Tree, the most subsets that contain complementary literal(s) can never be produced, and the true resolutions cannot be missed by pruning either. Then the concept of complementary degree is presented in this paper, and the nodes of SE-Tree are extended in accordance with the descending order of complementary degree. With this extended order, the subsets that contain complementary literal(s) and have smaller size can not only be generated early, but also can reduce the number of generated nodes that are redundant. Moreover the calculation for deciding the complementarity of subsets is reduced. Results show that the corresponding algorithm runs faster than CER algorithm and further improves the solving efficiency of problems which complementary factor is lower.

Key words: extension rule, model counting, CER (counting models using extension rules) algorithm, complementary degree, SE-Tree (set enumeration tree)