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

基于DPLL的SAT算法的研究及应用

作　者: 陈稳
导　师: 闫炜
学　校: 电子科技大学
专　业: 计算机软件与理论
关键词: 可满足性问题 可满足性算法 完备算法 局部搜索算法 DPLL
分类号: TP301.6
类　型: 硕士论文
年　份: 2011年
下　载: 83次
引　用: 0次
阅　读: 论文下载
 

内容摘要


命题逻辑公式的可满足性问题(SAT)是数理逻辑、计算机科学、集成电路设计与验证和人工智能等领域中的核心问题,并且是第一个被证明出来的NP问题。SAT问题在计算复杂性理论中具有非常重要的地位,设计并实现解决该类问题的高效算法意义重大。但目前不存在一种求解算法在最坏情况下的时间复杂度是多项式级别,其求解速度仍是制约SAT算法发展的一大难题。因此,世界各国的学者都在努力研究新的求解算法,以寻求出一种高效的求解算法。SAT算法分为完备算法和局部搜索算法这两类。其中,完备算法能给出命题逻辑公式的解或证明公式是不可满足的,但是效率较低;而局部搜索算法求解速度相对较快,但是不一定能够找到对应SAT问题的解。本文在对比分析这两类算法的基础上,对DPLL算法进行了改进,并通过实验证明了改进后算法的优越性。基于上述思想,本文的研究工作主要包括:(1)深入分析了基于DPLL的完备性SAT算法的实现原理,给出了算法思想和详细的实现过程,并对该算法中所使用到的数据结构和一些关键技术(加速搜索的启发式策略、子句删除机制、随机重启动机制)给予总结和分析。(2)结合完备算法能够进行完备求解和局部搜索算法能够以较快速度进行求解的优点,在DPLL这一基本算法框架之上提出了一种混合的SAT求解器,将局部搜索算法WALKSAT作为一个必要步骤融入到DPLL算法的求解过程中。一方面,WALKSAT算法得出的近似解可以指导DPLL对决策变量进行赋值,从而减小对决策变量赋值的随机性和盲目性;另一方面,每当顶层变量的赋值确定后,都引入WALKSAT对算法进行加速,从而提高求解效率。(3)改进DPLL算法的整体框架和实现,给出了改进后算法的框架和实现步骤,并选取一些难的随机SAT实例对改进前后的算法进行了测试,实验结果表明,改进后的算法对于求解可满足的随机3-SAT实例效果显著。(4)将改进后的算法应用到图论中的实际问题--四色问题。问题通过编码转换为CNF公式的形式后,输入到改进后的DPLL求解器中进行求解,并最终转换为对应的着色方案。实验表明,算法在极短的时间内就得出了四色问题的解。

全文目录


摘要  4-5
ABSTRACT  5-9
图目录  9-10
表目录  10-11
缩略语说明表  11-12
第一章 绪论  12-18
  1.1 课题研究背景及出发点  12
  1.2 SAT 问题研究意义  12-14
  1.3 可满足性问题的研究现状及挑战  14-16
  1.4 主要研究内容  16-17
  1.5 本文结构及内容安排  17-18
第二章 SAT 基本知识及相关算法  18-27
  2.1 算法的复杂度  18
  2.2 P 类与NP 类问题  18-20
  2.3 布尔表达式（布尔代数）  20
  2.4 范式相关概念  20-21
  2.5 SAT 问题的基本定义和性质  21-23
  2.6 SAT 问题相关算法  23-26
    2.6.1 完备算法  23-24
    2.6.2 局部搜索算法  24-25
    2.6.3 完备算法和局部搜索算法的对比  25-26
  2.7 小结  26-27
第三章 基于DPLL 的完备性SAT 算法研究  27-48
  3.1 使用的数据结构  27-32
    3.1.1 邻接表  27-30
    3.1.2 胀缩数据结构  30-32
  3.2 SAT 问题预处理  32-33
  3.3 加速搜索的一些启发式策略  33-40
    3.3.1 BCP（Boolean Constraint Propagation，布尔约束传播）  33-34
    3.3.2 变量决策策略  34-37
    3.3.3 冲突分析、子句学习、回溯机制  37-40
  3.4 子句删除机制  40-41
  3.5 随机重启动机制  41
  3.6 基于DPLL 的算法发展历史综述  41-43
  3.7 基于DPLL 的SAT 算法框架  43-47
    3.7.1 算法的基本思想  43-44
    3.7.2 实现过程  44-47
  3.8 小结  47-48
第四章 WM 算法——改进后的DPLL 算法  48-60
  4.1 算法描述  48-54
    4.1.1 算法思想分析  49-51
    4.1.2 WM 算法执行流程  51-54
  4.2 算法改进前后性能对比  54-58
    4.2.1 仿真环境  54
    4.2.2 测试用例  54-55
    4.2.3 仿真结果对比和分析  55-58
  4.3 算法复杂度分析  58
  4.4 小结  58-60
第五章 WM 算法的具体应用  60-66
  5.1 四色问题简介  60-61
  5.2 四色问题到SAT 问题的转换  61-64
  5.3 应用WM 算法进行求解  64-65
  5.4 小结  65-66
第六章 总结与展望  66-68
  6.1 本文工作总结  66-67
  6.2 下一步工作的展望  67-68
致谢  68-69
参考文献  69-72
个人简历  72-73

相似论文

  1. 开源软件依赖可满足性识别方法研究与实现,TP311.52
  2. 应用于集成电路形式化验证的SAT算法研究,TN402
  3. DNA自组装计算模型的应用研究,O242.1
  4. 基于进化非选择算法的可满足性问题求解,TP18
  5. 纵览传播算法求解随机3-SAT问题,TP18
  6. 基于回归分析和DCM模型的可满足性问题求解算法,TP301.6
  7. 超宽带小步进频率合成技术研究,TN74
  8. 可满足性问题算法研究-CNF的简化,TP301.6
  9. 基于子句权重求解SAT问题,TN402
  10. 基于FPGA的逆变电源控制器的研究,TM571
  11. 对可满足性（SAT）问题求全解的算法研究及实现,TP301.6
  12. 一种新的基于扩展规则的知识编译方法,TP182
  13. 离散数学中NP完全问题的DNA计算,TP301.6
  14. 基于SAT的VLSI测试向量自动生成技术,TN402
  15. 启发式将3-SAT化为2-SAT的DPLL算法,TP301.6
  16. 带随机步的可满足性算法,TP301.6
  17. 求解基约束下上模函数最小值的局部搜索算法及其性能保证,O224
  18. 可满足性问题和图染色的一些研究,TP301.6
  19. 粗集决策表属性约简算法的研究,TP18
  20. 用遗传算法解决3-SAT问题,TP18

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法 > 算法理论
© 2012 www.xueweilunwen.com