| 致谢 | 第1-6页 |
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-11页 |
| 1 引言 | 第11-19页 |
| ·课题研究的背景和意义 | 第11-12页 |
| ·研究领域的历史与现状 | 第12-17页 |
| ·SAT问题的发展趋势 | 第12-14页 |
| ·SMT问题的发展趋势 | 第14-16页 |
| ·基于可满足性求解器的优化问题的发展趋势 | 第16-17页 |
| ·课题研究的内容 | 第17页 |
| ·论文主要内容安排 | 第17-19页 |
| 2 搜索算法的发展研究 | 第19-26页 |
| ·基本定义与概念 | 第19-20页 |
| ·公式的可满足性 | 第20-21页 |
| ·搜索过程结构 | 第21-22页 |
| ·搜索算法结构 | 第22-26页 |
| 3 冲突分析算法 | 第26-43页 |
| ·标准冲突分析算法 | 第27-29页 |
| ·故障驱动的断言 | 第27-28页 |
| ·冲突导向的回溯 | 第28-29页 |
| ·标准冲突分析算法的不同版本 | 第29-32页 |
| ·空间限制的冲突分析算法 | 第30页 |
| ·Unique Implication Points | 第30-32页 |
| ·冲突分析改进算法 | 第32-37页 |
| ·设计思想 | 第32-35页 |
| ·算法设计 | 第35-37页 |
| ·冲突分析算法相关实验 | 第37-43页 |
| 4 子句预处理算法 | 第43-55页 |
| ·CNF范式的演绎能力 | 第43-48页 |
| ·基于CNF范式演绎能力的预处理算法 | 第48-52页 |
| ·子句预处理算法相关实验 | 第52-55页 |
| 5 适用于优化问题的SMT求解器 | 第55-65页 |
| ·预备知识 | 第55-56页 |
| ·有关CNF范式 | 第55页 |
| ·针对SMT问题的DPLL结构 | 第55-56页 |
| ·极值的必要条件 | 第56-58页 |
| ·二元函数 | 第56-57页 |
| ·多元函数 | 第57-58页 |
| ·针对优化问题的SMT求解器 | 第58-63页 |
| ·适用于优化问题的SMT算法相关实验 | 第63-65页 |
| 6 总结与展望 | 第65-67页 |
| ·论文工作总结 | 第65-66页 |
| ·工作展望 | 第66-67页 |
| 参考文献 | 第67-70页 |
| 作者简历 | 第70-72页 |
| 学位论文数据集 | 第72页 |