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