基于蕴含推理的SAT预处理器的实现
| 摘要 | 第1-5页 |
| Abstract | 第5-6页 |
| 引言 | 第6-7页 |
| 第一章 可满足问题概论 | 第7-10页 |
| ·问题与算法 | 第7-8页 |
| ·可满足问题 | 第8-9页 |
| ·论文概要 | 第9-10页 |
| 第二章 可满足问题的应用 | 第10-19页 |
| ·可满足问题的定义 | 第10-11页 |
| ·可满足问题的应用 | 第11-12页 |
| ·可满足问题在EDA中的应用 | 第12-18页 |
| ·ATPG | 第12-13页 |
| ·形式验证 | 第13-16页 |
| ·模型检验 | 第16页 |
| ·等价检验 | 第16-17页 |
| ·逻辑电路的CNF表示 | 第17-18页 |
| ·在EDA领域更多的应用 | 第18页 |
| ·小结 | 第18-19页 |
| 第三章 可满足问题的算法发展 | 第19-28页 |
| ·可满足问题的算法 | 第19-22页 |
| ·完备性算法 | 第19-21页 |
| ·非完备性算法 | 第21-22页 |
| ·完备性算法和非完备性算法的比较 | 第22页 |
| ·一些非传统的可满足问题算法 | 第22-26页 |
| ·模拟退火算法 | 第23页 |
| ·禁忌搜索 | 第23-24页 |
| ·遗传算法 | 第24-26页 |
| ·预处理器介绍 | 第26-28页 |
| 第四章 合取范式的简化 | 第28-36页 |
| ·逻辑蕴含推理 | 第28-31页 |
| ·基本概念及性质 | 第28-29页 |
| ·强制赋值 | 第29-31页 |
| ·等价变量 | 第31页 |
| ·蕴含图及对称性 | 第31-32页 |
| ·逻辑蕴含矩阵 | 第32-36页 |
| ·从合取范式到逻辑蕴含矩阵 | 第33-34页 |
| ·逻辑蕴含矩阵的化简 | 第34-36页 |
| 第五章 预处理器的算法和实现 | 第36-53页 |
| ·基本思想 | 第36-37页 |
| ·算法 | 第37-44页 |
| ·一元子句扩展 | 第38-39页 |
| ·文字与索引 | 第39页 |
| ·传播闭包 | 第39-41页 |
| ·强制文字和等价文字检查 | 第41-44页 |
| ·数据结构 | 第44-47页 |
| ·数据类 | 第44-46页 |
| ·控制类 | 第46-47页 |
| ·实验结果 | 第47-53页 |
| 第六章 总结与展望 | 第53-55页 |
| ·工作总结 | 第53-54页 |
| ·未来工作展望 | 第54-55页 |
| 后记 致谢 | 第55-56页 |
| 参考文献 | 第56-60页 |
