一个基于CNF约束的可满足问题简化的预处理解决器

摘要

随着集成电路设计和制造技术的不断进步，电路的规模也不断增大，电路验证和测试领域面临着前所未有的挑战。传统的基于模拟的验证方法不能满足电路复杂度增大的需要，具有完备性特点的形式化验证方法开始得到人们的关注，成为当前的研究热点。 本文研究工作是针对可满足问题(SAT)在组合电路验证和测试中的应用展开的。近些年来，作为验证基本问题的可满足性问题研究取得了重大进展，有效的SAT解决器诸如Zchaff，BerkMin和C-SAT等已可解决很大规模SAT问题。本文分析介绍了这些SAT解决器的算法和设计特点，针对其中的CNF简化预处理T作提出了改进的方法，能够提高整个问题的解决效率。 本文主要的创新之处在于：(1)使用二元关系矩阵来构建逻辑蕴含图和推导逻辑蕴含关系；(2)结合高级逻辑推导技术推进简化过程。从实验分析表明，这些措施能够有效提整个高解决SAT问题的效率，同时能够独立发现问题是否可满足。

目录

文摘

英文文摘

论文独创性声明及使用授权声明

第一章 绪论

1.1集成电路设计与制造技术的发展

1.2可满足问题(SAT)的应用背景

1.3可满足问题(SAT)的研究内容

1.4合取范式(CNF)预处理的研究情况

1.5本文的在合取范式简化预处理方面的改进尝试和主要贡献

1.6论文的组织结构

第二章 可满足问题在电路验证中的应用

2.1逻辑电路向CNF的转化

2.2基于SAT的电路等价验证

2.3基于SAT的电路故障测试

2.4其他基于SAT的形式验证

2.5小结

第三章 可满足问题的解决算法和解决器

3.1可满足问题的定义

3.2 BDD算法

3.3 DPLL算法

3.4 Zchaff解决器

3.4.1 BCP过程的数据结构

3.4.2冲突分析和学习过程

3.4.3变量的选择策略

3.4.4新加入子句的删除策略和定时重启策略

3.5小结

第四章 利用逻辑蕴含进行合取范式简化

4.1 SAT的逻辑蕴含关系

4.2逻辑蕴含关系的公理推导

4.3逻辑蕴含图

4.4 2-Simplify简介

4.5小结

第五章 简化预处理解决器的算法和实现

5.1目标

5.2 SPP的算法

5.2.1理论基础

5.2.2算法流程

5.2.3基于二元关系矩阵的逻辑蕴含关系推导

5.3数据结构

5.3.1数据结构类间的关系

5.3.2基础类

5.3.3控制类

5.3.4基于C++ STL的实现

5.4实验结果

第六章 总结与展望

6.1 工作总结

6.2未来工作展望

参考文献

致谢