| 摘要 | 第6-8页 |
| Abstract | 第8-10页 |
| 第1章 绪论 | 第19-32页 |
| 1.1 选题背景及意义 | 第19-20页 |
| 1.2 国内外相关研究现状 | 第20-28页 |
| 1.2.1 DPLL(Davis-Putnam-Logemann-Loveland)算法框架 | 第21-23页 |
| 1.2.2 CDCL(Conflict-DrivenClauseLearning)求解系统 | 第23-27页 |
| 1.2.3 基于归结方法的求解系统 | 第27-28页 |
| 1.3 论文的主要工作 | 第28-30页 |
| 1.4 论文结构安排 | 第30-32页 |
| 第2章 基于矛盾体分离的命题逻辑动态自动演绎推理 | 第32-42页 |
| 2.1 引言 | 第32页 |
| 2.2 预备知识 | 第32-35页 |
| 2.2.1 SAT(Satisfiability,可满足性)问题 | 第32-33页 |
| 2.2.2 线性归结演绎 | 第33-34页 |
| 2.2.3 基于矛盾体分离的动态自动演绎推理原理 | 第34-35页 |
| 2.3 基于矛盾体分离的命题逻辑自动演绎推理系统实现 | 第35-40页 |
| 2.3.1 基于最大矛盾体构造的动态自动演绎推理求解系统 | 第35-37页 |
| 2.3.2 基于分解的动态自动演绎推理求解系统 | 第37-39页 |
| 2.3.3 与主流CDCL求解器融合的自动演绎推理求解系统 | 第39-40页 |
| 2.4 小结 | 第40-42页 |
| 第3章 基于矛盾体重构的子句学习算法 | 第42-58页 |
| 3.1 引言 | 第42页 |
| 3.2 子句学习技术研究背景 | 第42-44页 |
| 3.2.1 基于归结原理的学习子句生成方法 | 第42页 |
| 3.2.2 基于蕴涵图分析的学习子句生成方法 | 第42-44页 |
| 3.3 基于矛盾体重构的子句学习算法 | 第44-54页 |
| 3.3.1 线性归结演绎扩展 | 第44-51页 |
| 3.3.2 与FirstUIP分割方法比较 | 第51-54页 |
| 3.4 实验结果分析 | 第54-57页 |
| 3.5 小结 | 第57-58页 |
| 第4章 基于矛盾体分离的扩充求解算法 | 第58-71页 |
| 4.1 引言 | 第58页 |
| 4.2 单一分支决策的局限性 | 第58-60页 |
| 4.3 基于线性归结演绎的局部解成组提取 | 第60-68页 |
| 4.3.1 成组提取局部解的基本原理 | 第60-63页 |
| 4.3.2 成组提取局部解的过程及实现算法 | 第63-65页 |
| 4.3.3 逻辑演绎分组示例 | 第65-68页 |
| 4.4 实验结果分析 | 第68-70页 |
| 4.5 小结 | 第70-71页 |
| 第5章 基于动态评估的启发式文字选择算法 | 第71-86页 |
| 5.1 引言 | 第71页 |
| 5.2 决策文字选择算法研究背景 | 第71-73页 |
| 5.3 基于冲突比率的启发式文字选择算法 | 第73-77页 |
| 5.3.1 变元活跃度与决策层、冲突次数的相关性 | 第73-75页 |
| 5.3.2 分支变元活跃度综合评估 | 第75-77页 |
| 5.4 实验结果 | 第77-84页 |
| 5.4.1 Minisat+DA与Minisat+EVSIDS对比 | 第77-81页 |
| 5.4.2 MapleCOMSPS+DA与MapleCOMSPS+EVSIDS对比 | 第81-83页 |
| 5.4.3 结果分析 | 第83-84页 |
| 5.5 小结 | 第84-86页 |
| 第6章 演绎结果评估算法 | 第86-108页 |
| 6.1 引言 | 第86页 |
| 6.2 演绎结果评估算法研究背景 | 第86-87页 |
| 6.3 基于冲突分析频率的学习子句删除算法 | 第87-96页 |
| 6.3.1 学习子句与搜索过程的相关度分析 | 第87-89页 |
| 6.3.2 学习子句参与冲突分析的频率对搜索的影响 | 第89-96页 |
| 6.4 学习子句动态趋势评估算法 | 第96-107页 |
| 6.4.1 学习子句被用于冲突分析的时间分布 | 第96-100页 |
| 6.4.2 累积趋势强度实现算法 | 第100-101页 |
| 6.4.3 对比实验 | 第101-107页 |
| 6.5 小结 | 第107-108页 |
| 第7章 基于向量空间模型的搜索路径识别算法 | 第108-124页 |
| 7.1 引言 | 第108页 |
| 7.2 路径识别及重启算法研究背景 | 第108-113页 |
| 7.2.1 已搜索路径增长规律 | 第108-110页 |
| 7.2.2 搜索路径识别方法 | 第110-111页 |
| 7.2.3 重启算法 | 第111-113页 |
| 7.3 基于改进向量空间模型的搜索路径识别 | 第113-116页 |
| 7.3.1 决策层对搜索路径的影响 | 第113-114页 |
| 7.3.2 基于向量空间模型的搜索路径识别算法 | 第114-116页 |
| 7.4 实验结果 | 第116-123页 |
| 7.4.1 Minisat嵌入路径识别算法前后性能对比 | 第116-119页 |
| 7.4.2 MapleCOMSPS嵌入路径识别算法前后性能对比 | 第119-123页 |
| 7.4.3 结果分析 | 第123页 |
| 7.5 小结 | 第123-124页 |
| 第8章 总结与展望 | 第124-127页 |
| 8.1 论文总结 | 第124-125页 |
| 8.2 今后工作展望 | 第125-127页 |
| 致谢 | 第127-128页 |
| 参考文献 | 第128-138页 |
| 攻读博士学位期间发表的论文及科研成果 | 第138-139页 |
| 攻读博士学位期间主研的科研项目 | 第139页 |
