可满足性问题DPLL算法研究

摘要

近十多年来随着许多有效的启发式算法的提出以及一系列数据结构和实现方法上的创新使得可满足性问题(SAT)的求解水平取得了突飞猛进的提高。尽管目前可满足性问题还属于NP问题，目前还没有任何一种算法能实现在最差情况下的多项式时间复杂度，但当前的SAT问题求解器以能够轻松解决含有几万个甚至几十万个变量的可满足性问题。由于可满足性问题求解水平的巨大进步，SAT的应用范围已越来越大，从形式验证到人工智能等许多领域均以SAT求解器作为其核心计算引擎。可满足性问题的研究已经从一个计算机理论学界的纯学术问题逐渐发展成为当前许多计算机领域中具有很大应用价值的计算问题。 本论文的贡献在于总结和分析了那些推动SAT问题发展的最主要的启发式算法和技术，并在此基础上提出了两点创新。其一，提出了一种新的正向推理技术：对称扩展的一元子句推导。与传统的一元子句推导技术相比，本文的方法通过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句。基于这项技术本文实现了一个可满足性问题预处理器Snowball。实验结果验证了这项新的正向推理技术的有效性，并表明该预处理器Snowball能够有效地化简SAT问题的规模并减少解决SAT问题的时间，特别是对不满足问题有不少例子可直接得到结果。其二，本文首次提出了一种采用双变量决策策略的可满足性问题DPLL算法以及其完整的实现方式描述。采用双变量决策策略能在理论上减少决策级数，进而能有效地减少SAT问题的搜索空间，加速SAT问题的求解。该双变量决策SAT算法的实现是以Minisat解决器为蓝本的。在其较完善的DPLL算法框架内本文对其中的各个主要的功能模块均进行了改造，使得改造后的SAT解决器首次具有了双变量决策功能，并与其中主要的软件模块：变量决策模块，蕴含推理模块，冲突分析和回溯模块相互配合，协调一致。实验结果验证了算法的正确性。

目录

文摘

英文文摘

声明

第1章绪论

1.1集成电路验证危机与SAT问题

1.2 SAT问题研究现状和挑战

1.3本文的主要贡献

1.4论文组织结构

第2章基础知识

2.1布尔逻辑代数

2.2计算复杂度

2.3 SAT问题的表示和定义

2.4电路验证与SAT问题转换

第3章可满足性问题DPLL算法的发展

3.1历史回顾

3.2 SAT预处理方法

3.3搜索的启发式策略

3.4数据结构

3.5小结

第4章对称蕴含预处理算法

4.1对称扩展的一元推导

4.2推理闭包的实现

4.3预处理器Snowball算法

4.4实验结果和分析

第5章双变量决策DPLL算法

5.1算法目的

5.2决策模块

5.3蕴含推理模块

5.4冲突分析和回溯模块

5.5数据结构

5.6实验结果

第6章总结与展望

6.1论文工作总结

6.2对后续工作的展望

参考文献

硕士期间撰写或参与撰写的论文

致谢