ISSN 1000-1239 CN 11-1777/TP

• 人工智能 •

### 结合互补度的基于扩展规则#SAT问题求解方法

1. (吉林大学计算机科学与技术学院 长春 130012) (符号计算与知识工程教育部重点实验室(吉林大学) 长春 130012) (ouyd@jlu.edu.cn)
• 出版日期: 2016-07-01
• 基金资助:
国家自然科学基金项目(61402196,61272208,61133011,61003101,61170092)；中国博士后科学基金项目(2013M541302)；吉林省科技发展计划基金项目(20140520067JH)

### 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

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.