【摘要】 最坏情况下#SAT问题上界的研究已成为一个热门的研究领域.#SAT问题的时间复杂性是根据问题实例的大小所组成的函数计算所得.#SAT问题实例的大小不仅依赖于变量的数量,还依赖于子句的数量.以子句数量为参数研究#SAT问题在最坏情况下的上界,不仅可以从另一个角度衡量算法的好坏,而且在某种程度上更能准确地反映出算法的性能.首先从子句数量的角度证明了之前提出的基于扩展规则的模型计数算法(CER算法)的上界O(2m),其中m是公式中子句的数量.为了提高#3-SAT问题的求解效率,采用了多种分裂规则,进一步给出了一种基于Davis-Putnam-Logemann-Loveland(DPLL)的#3-SAT算法MCDP.通过分析该算法得到了以子句数量为参数的#3-SAT问题在最坏情况下的上界O(1.8393m).更多还原

【Abstract】 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 worst-case upper bound O(1.8393m) for #3-SAT,where m is the number of clauses in a formula.更多还原