对称扩展一元子句推导与双变量DPLL算法：SAT求解的创新突破

本论文深入探讨了可满足性问题（SAT）领域的最新进展，尤其是在DPLL算法（Davis-Putnam-Logemann-Loveland）优化上的创新。作者熊伟在复旦大学攻读硕士学位期间，针对SAT问题求解中的关键瓶颈，提出了两项关键贡献。 首先，论文提出了一种新颖的正向推理技术——对称扩展的一元子句推导。传统的单个一元子句推导技术通常处理的是单向逻辑关系，而这种新方法引入了对称的蕴涵关系，这使得在推导过程中能够挖掘出更多的潜在信息，从而构建更丰富的子句集。作者开发的预处理器Snowball就是基于这项技术实现的，实验结果显示，它显著地简化了SAT问题的规模，特别是在处理不满足问题时，能快速得出结果，提高了求解效率。 其次，论文实现了创新性的双变量决策策略的DPLL算法。相比于传统的单变量决策策略，双变量决策策略理论上可以减少决策级数，减小SAT问题的搜索空间，从而加速求解过程。作者的设计是基于Minisat解决器的，对DPLL算法的核心模块如变量决策、蕴含推理、冲突分析和回溯等进行了优化改造，赋予了解决器双变量决策的能力。这种改进后的SAT解决器在实践中证明了其正确性和有效性。 这些创新不仅提升了SAT问题求解的性能，而且拓宽了SAT技术在形式验证、人工智能等领域的应用可能性。随着SAT技术的不断演进，它已成为计算机科学领域中具有实际应用价值的重要工具。通过本论文的研究，熊伟展示了如何通过理论与实践相结合，推动可满足性问题的解决技术向着更加高效和精确的方向发展。