可满足模理论解决器--拟人拟物算法研究
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第一章 绪论 | 第7-10页 |
| ·研究背景和意义 | 第7-8页 |
| ·本论文的主要工作及安排 | 第8-10页 |
| 第二章 可满足模理论及其解决器 | 第10-24页 |
| ·可满足模理论简介 | 第10-14页 |
| ·命题逻辑 | 第10-11页 |
| ·一阶逻辑的类型化 | 第11-12页 |
| ·理论 | 第12-13页 |
| ·常见理论 | 第13-14页 |
| ·可满足模理论解决器的实现框架及方法 | 第14-19页 |
| ·Eager 框架 | 第15-16页 |
| ·Lazy 框架 | 第16-17页 |
| ·Nelson-Oppen 组合理论 | 第17-19页 |
| ·SMT-LIB 和 SMT 国际大赛 | 第19-20页 |
| ·主流的 SMT 解决器 | 第20-23页 |
| ·本章小结 | 第23-24页 |
| 第三章 OpenSMT 解决器 | 第24-42页 |
| ·Tseitin 编码与同余闭包 | 第24-25页 |
| ·Tseitin 编码 | 第24-25页 |
| ·同余闭包 | 第25页 |
| ·OpenSMT 简介 | 第25-27页 |
| ·OpenSMT 软件结构 | 第27-30页 |
| ·OpenSMT 数据结构 | 第30-32页 |
| ·OpenSMT 数据结构状态举例 | 第32-33页 |
| ·主要算法 | 第33-41页 |
| ·MiniSAT | 第33-34页 |
| ·理论解决器 | 第34页 |
| ·SAT 解决器与理论解决器互动机制 | 第34-41页 |
| ·本章小结 | 第41-42页 |
| 第四章 GHSMT 解决器 | 第42-52页 |
| ·拟人拟物算法 | 第42-43页 |
| ·算法思想 | 第42页 |
| ·算法描述及步骤 | 第42-43页 |
| ·GHSMT 解决器的实现 | 第43-47页 |
| ·算法整合动机 | 第43-44页 |
| ·算法策略及流程 | 第44-47页 |
| ·Benchmarks 测试及结果分析 | 第47-51页 |
| ·测试 Benchmarks | 第47页 |
| ·测试平台 | 第47页 |
| ·参数设置 | 第47页 |
| ·实验结果讨论 | 第47-51页 |
| ·本章小结 | 第51-52页 |
| 第五章 总结与展望 | 第52-53页 |
| ·本文工作总结 | 第52页 |
| ·未来的工作 | 第52-53页 |
| 参考文献 | 第53-58页 |
| 附录 | 第58-86页 |
| 致谢 | 第86-87页 |
| 攻读硕士期间参与的科研项目 | 第87-88页 |
| 攻读硕士期间发表的学术论文 | 第88页 |
