| 摘要 | 第5-7页 |
| Abstract | 第7-8页 |
| 第1章 引言 | 第14-26页 |
| 1.1 研究背景和意义 | 第14-15页 |
| 1.2 SAT问题 | 第15-17页 |
| 1.3 国内外研究现状 | 第17-22页 |
| 1.3.1 SAT问题编码方法 | 第17-18页 |
| 1.3.2 SAT问题的预处理技术 | 第18-19页 |
| 1.3.3 SAT问题的求解算法 | 第19-22页 |
| 1.4 SAT求解面临的挑战 | 第22页 |
| 1.5 研究内容 | 第22-24页 |
| 1.6 论文组织 | 第24-26页 |
| 第2章 相关技术 | 第26-38页 |
| 2.1 预处理方法SATELITE | 第26-27页 |
| 2.2 确定性SAT求解算法CDCL | 第27-29页 |
| 2.3 随机搜索SAT求解算法SLS | 第29-31页 |
| 2.4 进化算法ABC | 第31-34页 |
| 2.5 流行SAT求解算法比较 | 第34-37页 |
| 2.6 本章小结 | 第37-38页 |
| 第3章 基于SATELITE改进的预处理方法 | 第38-66页 |
| 3.1 基于动态约束和启发式选择的变量消除解析 | 第38-47页 |
| 3.1.1 RCS-VER子句状态动态约束 | 第39-44页 |
| 3.1.2 HVC-VER解析变量选择启发式 | 第44-47页 |
| 3.2 基于冲突检测学习和启发式选择的二元子句探针 | 第47-54页 |
| 3.2.1 CBCP二元子句探针化简规则 | 第48-53页 |
| 3.2.2 HVC-PRB探针变量选择启发式 | 第53-54页 |
| 3.3 实验与分析 | 第54-64页 |
| 3.3.1 实验设计 | 第55-56页 |
| 3.3.2 预处理性能对比分析 | 第56-60页 |
| 3.3.3 求解性能对比分析 | 第60-64页 |
| 3.4 本章小结 | 第64-66页 |
| 第4章 2W动态启发式重启策略 | 第66-104页 |
| 4.1 基于CDCL的重启策略 | 第66-70页 |
| 4.1.1 静态重启策略 | 第67-68页 |
| 4.1.2 动态重启策略 | 第68-70页 |
| 4.2 When重启 | 第70-78页 |
| 4.2.1 基本思想 | 第70-76页 |
| 4.2.2 When重启实现 | 第76-78页 |
| 4.3 Where重启 | 第78-83页 |
| 4.3.1 基本思想 | 第78-81页 |
| 4.3.2 Where重启实现 | 第81-83页 |
| 4.4 基于When和Where重启策略的求解算法 | 第83-85页 |
| 4.5 实验与分析 | 第85-103页 |
| 4.5.1 实验设计 | 第85页 |
| 4.5.2 基于CDCL的重启策略对比分析 | 第85-93页 |
| 4.5.3 2WSAT求解性能分析 | 第93-103页 |
| 4.6 本章小结 | 第103-104页 |
| 第5章 基于人工蜂群的SAT求解算法 | 第104-130页 |
| 5.1 基于ABC的SAT问题求解 | 第104-108页 |
| 5.1.1 基本思想 | 第104页 |
| 5.1.2 构成要素 | 第104-108页 |
| 5.2 ABCSAT算法 | 第108-121页 |
| 5.2.1 初始解 | 第108-109页 |
| 5.2.2 适应度函数 | 第109-110页 |
| 5.2.3 邻域选择策略 | 第110-111页 |
| 5.2.4 新解生成策略 | 第111-114页 |
| 5.2.5 跟随蜂选择策略 | 第114页 |
| 5.2.6 禁忌搜索 | 第114-118页 |
| 5.2.7 ABCSAT算法描述 | 第118-121页 |
| 5.3 实验与分析 | 第121-129页 |
| 5.3.1 实验设计 | 第121-122页 |
| 5.3.2 不同策略对比分析 | 第122-125页 |
| 5.3.3 求解性能对比分析 | 第125-129页 |
| 5.4 本章小结 | 第129-130页 |
| 第6章 NP类注释传播问题SAT归约 | 第130-146页 |
| 6.1 注释传播问题 | 第130-134页 |
| 6.1.1 视图副作用 | 第130-132页 |
| 6.1.2 来源副作用 | 第132-133页 |
| 6.1.3 注释放置问题 | 第133-134页 |
| 6.2 NP类视图副作用问题归约到SAT问题 | 第134-140页 |
| 6.2.1 JU查询视图副作用归约 | 第134-137页 |
| 6.2.2 PJ查询视图副作用归约 | 第137-140页 |
| 6.3 NP类来源副作用问题归约到SAT问题 | 第140-141页 |
| 6.3.1 JU查询来源副作用归约 | 第141页 |
| 6.3.2 PJ查询来源副作用归约 | 第141页 |
| 6.4 NP类注释放置问题归约到SAT问题 | 第141-144页 |
| 6.5 有效性分析 | 第144页 |
| 6.6 本章小结 | 第144-146页 |
| 第7章 总结与展望 | 第146-150页 |
| 7.1 本文主要工作总结及创新 | 第146-147页 |
| 7.2 SAT问题研究展望及未来工作 | 第147-150页 |
| 参考文献 | 第150-160页 |
| 致谢 | 第160-162页 |
| 攻读学位期间发表的论文 | 第162页 |