可满足性问题DPLL算法研究

本论文的贡献在于总结和分析了那些推动SA=r问题发展的最主要的启发式 算法和技术，并在此基础上提出了两点创新。其一，提出了一种新的正f剐燕理技 术：对称扩展的一元子旬推导。与传统的一元子句推导技术相比，本文的方法通 过在一元子句推导过程中添加对称的蕴涵关系从而能够推导出更多的一元子句。 基于这项技术本文实现了一个可满足性问题预处理器Snowball。实验结果验证了 这项新的正向推理技术的有效性，并表明该预处理器Snowball能够有效地化简 SAT问题的规模并减少解决SAT问题的时间，特别是对不满足问题有不少例子可 直接得到结果。其二，本文首次提出了一种采用双变量决策策略的可满足性问题 DPLL算法以及其完整的实现方式描述。采用双变量决策策略能在理论上减少决 策级数，进而能有效地减少SAT问题的搜索空间，加速SAT问题的求解。该双变 量决策SAT算法的实现是以Minisat解决器为蓝本的。在其较完善的DPLL算法框 架内本文对其中的各个主要的功能模块均进行了改造，使得改造后的SAT解决器 首次具有了双变量决策功能，并与其中主要的软件模块：变量决策模块，蕴含推 理模块，冲突分析和回溯模块相互配合，协调一致。实验结果验证了算法的正确 性。