最坏情况下#3-SAT问题最小上界  

Minimized Upper Bound for #3-SAT Problem in the Worst Case

作　　者：周俊萍[1,2] 殷明浩[2,3] 周春光[1] 翟延冬[1] 王康平[1] 

机构地区：[1]吉林大学计算机科学与技术学院,长春130012 [2]东北师范大学计算机科学与信息技术学院,长春130117 [3]教育部符号计算与知识工程重点实验室(吉林大学),长春130012

出　　处：《计算机研究与发展》2011年第11期2055-2063,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60673099;60773097;60803102;60873146)

摘　　要：最坏情况下#SAT问题上界的研究已成为一个热门的研究领域.#SAT问题的时间复杂性是根据问题实例的大小所组成的函数计算所得.#SAT问题实例的大小不仅依赖于变量的数量,还依赖于子句的数量.以子句数量为参数研究#SAT问题在最坏情况下的上界,不仅可以从另一个角度衡量算法的好坏,而且在某种程度上更能准确地反映出算法的性能.首先从子句数量的角度证明了之前提出的基于扩展规则的模型计数算法(CER算法)的上界O(2m),其中m是公式中子句的数量.为了提高#3-SAT问题的求解效率,采用了多种分裂规则,进一步给出了一种基于Davis-Putnam-Logemann-Loveland(DPLL)的#3-SAT算法MCDP.通过分析该算法得到了以子句数量为参数的#3-SAT问题在最坏情况下的上界O(1.8393m).Propositional model counting or # SAT is the problem of computing the number of models for a given propositional formula. The rigorous theoretical analysis of algorithms for solving #SAT have been proposed in the literature. The time complexity is calculated based on the size of the #SAT instances, depending on not only the number of variables, but also the number of clauses. Researches on the worst case upper bound for #SAT with the number of clauses as the parameter can not only measure the efficiency of the algorithms, but also correctly reflect their performance. Therefore, it is significant to exploit the minimized upper bound of #SAT problem in the worst case using the number of clauses as the parameter. In this paper, we firstly analyze the CER algorithm which we have proposed for solving #SAT and prove an upper bound O（2m） regarding the number of clauses as the parameter. In order to increase the efficiency, an algorithm MCDP based on Davis-Putnam-Logemann- Loveland （DPLL） for solving # 3-SAT is presented. By analyzing the algorithm, we obtain the worstcase upper bound O（1. 8393^m） for # 3-SAT, where m is the number of clauses in a formula.

关 键 词：最坏情况 上界 #3 SAT 复杂性分析 模型计数 

分 类 号：TP301.5[自动化与计算机技术—计算机系统结构]