学位论文 > 优秀研究生学位论文题录展示

基于DPLL的#SAT子类算法的研究

作　者: 王洪琳
导　师: 谷文祥
学　校: 东北师范大学
专　业: 计算机软件与理论
关键词: 智能规划 #SAT DPLL 时间复杂性上界
分类号: TP18
类　型: 硕士论文
年　份: 2013年
下　载: 2次
引　用: 0次
阅　读: 论文下载

内容摘要

智能规划是人工智能领域的一个前沿研究领域，近年来，对该领域的研究也取得了突破性的进展，研究人员提出了多种方法来求解该问题，其中一种非常高效的求解方法就是将智能规划问题转化成命题可满足性问题（简称SAT问题）。但是，在智能规划领域当中还有很多类经典规划问题，是不能通过转化成SAT问题来求解的，有的还需要计算命题公式的可满足赋值个数，因此衍生出了模型计数问题（简称#SAT问题）。在实际应用中，为了更加容易解决某些问题，研究者们通常会尽量将困难问题转化为逻辑结构尽量简单的命题公式。计算逻辑结构有所限制的命题公式的模型个数问题统称为#SAT子类问题，因此推动#SAT子类问题的研究，对智能规划乃至人工智能领域都有着极其深远的潜在应用价值。在目前求解SAT、#SAT及其子类问题的各种算法中，DPLL算法的性能是最为高效的，但是该算法的时间复杂度还是指数级别的，故，很多研究者在DPLL算法的基础上，通过提出新化简规则或者细化分支等多种手段进一步提高DPLL算法的性能，让该算法的性能获得指数级别的提高。同时，这种思想也催生了研究者们对SAT及其各种扩展问题的算法在最坏情况下，时间复杂性上界的关注。本文选择#SAT的一个子类问题—#2-SAT问题，作为研究课题，使用DPLL算法对目前时间复杂性上界最小的#2-SAT算法进行了改进，提出一种新算法—PMC算法。鉴于目前国内外大多以变量数目作为分析#SAT子类算法在最坏情况下的时间复杂性上界，本文还选择从子句数目角度出发，利用分支树方法计算分析PMC算法，将该算法在最坏情况下的时间复杂性上界从O(1.1892m)提高到O(1.1740m)。另外，根据PMC算法设计了#2-SAT求解器，并与原#2-SAT算法做了对比实验，实验结果表明，相同2-CNF公式进行求解，PMC算法的运行时间明显小于原#2-SAT算法。

全文目录

摘要  4-5
Abstract  5-6
目录  6-7
引言  7-9
第一章智能规划  9-11
  1.1 智能规划问题  9
  1.2 智能规划发展及现状  9-10
  1.3 智能规划方法  10-11
第二章模型计数问题  11-15
  2.1 命题可满足性问题  11-13
    2.1.1 SAT 问题的相关概念  11-12
    2.1.2 SAT 问题的求解方法  12
    2.1.3 有关 SAT 问题计算复杂性上界的研究  12-13
  2.2 模型计数问题  13-15
    2.2.1 #SAT 问题的相关概念  13
    2.2.2 #SAT 问题的求解方法  13-14
    2.2.3 关于#SAT 问题计算复杂性上界的研究  14-15
第三章基于 DPLL 的#2-SAT 算法  15-20
  3.1 图论的相关概念  15
  3.2 PMC 算法及其正确性  15-20
    3.2.1 化简规则  15-16
    3.2.2 PMC 算法设计及其正确性证明  16-20
第四章在最坏情况下 PMC 算法的最小上界  20-23
  4.1 分支树原理  20
  4.2 PMC 算法的时间复杂性分析  20-23
第五章实验对比测试  23-25
  5.1 开发工具及测试环境  23
  5.2 实验结果及分析  23-25
结论  25-27
参考文献  27-31
致谢  31-32
在学期间公开发表论文及著作情况  32

基于DPLL的#SAT子类算法的研究

内容摘要

全文目录

相似论文