位置:成果数据库 > 期刊 > 期刊详情页
最坏情况下#3-SAT问题最小上界
  • ISSN号:1000-1239
  • 期刊名称:计算机研究与发展
  • 时间:2011.11.11
  • 页码:2055-2063
  • 分类:TP301.5[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]吉林大学计算机科学与技术学院,长春130012, [2]东北师范大学计算机科学与信息技术学院,长春130117, [3]教育部符号计算与知识工程重点实验室吉林大学,长春130012
  • 相关基金:国家自然科学基金项目(60673099,60773097,60803102,60873146)
  • 相关项目:对象集合动态可变的应对规划研究
中文摘要:

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

英文摘要:

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.

同期刊论文项目
期刊论文 66 会议论文 2
期刊论文 48 会议论文 6
期刊论文 39 会议论文 7
同项目期刊论文
期刊信息
  • 《计算机研究与发展》
  • 中国科技核心期刊
  • 主管单位:中国科学院
  • 主办单位:中国科学院计算技术研究所
  • 主编:徐志伟
  • 地址:北京市科学院南路6号中科院计算所
  • 邮编:100190
  • 邮箱:crad@ict.ac.cn
  • 电话:010-62620696 62600350
  • 国际标准刊号:ISSN:1000-1239
  • 国内统一刊号:ISSN:11-1777/TP
  • 邮发代号:2-654
  • 获奖情况:
  • 2001-2007百种中国杰出学术期刊,2008中国精品科...,中国期刊方阵“双效”期刊
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,荷兰文摘与引文数据库,美国工程索引,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:40349