| 摘要 | 第3-4页 |
| ABSTRACT | 第4页 |
| 1 绪论 | 第8-10页 |
| 1.1 SAT问题的背景和意义 | 第8页 |
| 1.2 本文主要研究内容 | 第8-9页 |
| 1.3 本文工作的主要安排 | 第9-10页 |
| 2 SAT求解器的分类 | 第10-15页 |
| 2.1 按照算法特征的分类 | 第10-12页 |
| 2.1.1 完备算法 | 第10页 |
| 2.1.2 不完备算法 | 第10-12页 |
| 2.2 按照实现方法的分类 | 第12-14页 |
| 2.2.1 软件 | 第12-13页 |
| 2.2.2 硬件 | 第13-14页 |
| 2.2.2.1 ASIC | 第13页 |
| 2.2.2.2 FPGA | 第13-14页 |
| 2.3 本章小结 | 第14-15页 |
| 3 基于电路特征的SAT求解芯片 | 第15-26页 |
| 3.1 工具链 | 第15-16页 |
| 3.1.1 Xilinx ISE工具 | 第15页 |
| 3.1.2 CNF到电路的自动解析器 | 第15-16页 |
| 3.2 FPGA架构 | 第16-18页 |
| 3.2.1 逻辑生成器模块 | 第16-17页 |
| 3.2.2 激励模块 | 第17-18页 |
| 3.3 硬件求解流程 | 第18-19页 |
| 3.4 求解方法 | 第19-25页 |
| 3.4.1 顺序遍历激励求解 | 第19-21页 |
| 3.4.1.1 电路设计 | 第19-20页 |
| 3.4.1.2 实例分析 | 第20-21页 |
| 3.4.2 真随机数激励和伪随机数激励求解 | 第21-25页 |
| 3.4.2.1 引言 | 第21页 |
| 3.4.2.2 基于FPGA的大变量真随机数产生机制 | 第21-22页 |
| 3.4.2.3 基于FPGA的大变量伪随机数产生机制 | 第22-23页 |
| 3.4.2.4 实例分析 | 第23-25页 |
| 3.5 本章小结 | 第25-26页 |
| 4 基于DPLL的SAT求解芯片 | 第26-41页 |
| 4.1 随机前后溯的DPLL算法简介 | 第26-29页 |
| 4.1.1 算法的蕴含推理计算 | 第26页 |
| 4.1.2 DPLL算法结构 | 第26-27页 |
| 4.1.3 随机前后溯 | 第27-29页 |
| 4.1.3.1 随机变量搜索 | 第27-28页 |
| 4.1.3.2 随机变量赋值 | 第28-29页 |
| 4.2 工具链 | 第29-30页 |
| 4.3 FPGA架构 | 第30-31页 |
| 4.4 主要电路模块 | 第31-35页 |
| 4.4.1 蕴含推理及冲突检测电路 | 第31-33页 |
| 4.4.2 FSM电路 | 第33-35页 |
| 4.5 实例分析 | 第35-40页 |
| 4.5.1 实验环境 | 第35-38页 |
| 4.5.2 实验结果分析 | 第38-40页 |
| 4.6 本章小结 | 第40-41页 |
| 5 展望与总结 | 第41-42页 |
| 5.1 本文工作总结 | 第41页 |
| 5.2 未来的工作 | 第41-42页 |
| 参考文献 | 第42-46页 |
| 附录 | 第46-73页 |
| 致谢 | 第73-74页 |
| 攻读硕士期间发表的学术论文 | 第74-75页 |
| 攻读硕士期间参与的科研项目 | 第75页 |