基于DPLL的二进制数独SAT求解器设计与优化

本篇课程设计报告的主题围绕"基于SAT的二进制数独游戏求解程序"展开，属于数据结构领域的实践项目。该设计旨在通过实现DPLL算法来解决计算机科学与技术中的一个经典问题——命题逻辑公式的可满足性问题（SAT）。SAT问题在理论计算机科学中具有重要意义，它属于NP完全问题，常用于硬件设计、安全协议验证等领域。 学生孟彦康在计科校交1803专业班进行课程设计，由周全老师指导，报告日期为2020年2月1日。设计的核心内容涉及以下几个方面： 1. 公式解析与内部表示：设计程序能够读取以CNF范式表示的SAT算例文件，并将其解析成内部数据结构，如变量、词项、子句和公式。同时，程序需要具备验证解析正确性的功能，确保每一步都符合输入算例。 2. DPLL算法实现：基于DPLL算法，设计一个完备的SAT求解器，对CNF范式的问题实例进行求解。DPLL算法的关键在于有效的变量选择和子句处理策略，以提高求解效率。 3. 时间性能优化：通过优化存储结构和分支变元处理策略，提升程序执行效率。通过对比未优化前和优化后的执行时间，计算出明确的性能优化率。 4. 二进制数独游戏的SAT转化：将数独问题转化为SAT问题，这需要理解数独规则，并将其转化为逻辑表达式，以便于利用求解器求解。设计的游戏应具有互动性，用户可以输入初始状态并查看解决方案。 5. 参考文献：设计者引用了多本权威著作，如张健的《逻辑公式的可满足性判定》、Tanbir Ahmed的硕士论文《DPLL算法的实现》以及陈稳关于DPLL的SA相关研究，这些文献为设计提供了理论支持和技术指导。 这个课程设计不仅是对DPLL算法的实际应用，也锻炼了学生的编程技能、问题解决能力和理论知识的整合能力，展示了如何将理论知识与实际问题结合，创造出具有实用价值的软件工具。