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

在本次数据结构课程设计中，学生周大伟针对"基于SAT的二进制数独游戏求解程序"这一课题进行了深入研究。课程背景为程序设计综合课程设计，隶属于计科校交1803专业。设计的核心内容围绕SAT问题展开，即命题逻辑公式的可满足性判定，这是一个典型的NP完全问题，具有广泛的实际应用价值，如硬件设计和安全协议验证。 设计的目标是基于DPLL算法（Davis-Putnam-Logemann-Loveland算法）实现一个高效的SAT求解器。首先，需要从输入的CNF范式算例文件中解析出逻辑公式，并构建相应的物理存储结构，如变量、符号、子句和公式，以优化求解性能。设计要求包括输入输出功能，确保能够正确接收参数、读取文件、输出结果并保存。 此外，设计中需实现公式解析和验证功能，通过遍历内部结构并逐行输出子句，与原始输入进行对比，以确认解析的准确性。时间性能的测量是必不可少的，利用time.h中的时间处理函数记录DPLL算法的执行时间，并作为输出信息的一部分。 进一步的，设计者试图对基础DPLL算法进行优化，可能涉及到存储结构的改进或分支变元选取策略的调整，以提升程序效率。优化效果通过比较优化前后求解同一算例的时间，计算优化率来体现，优化率公式为(未优化时间-t/to)*100%。 课程设计还涉及了将二进制数独问题转化为SAT问题的技术，将游戏与SAT求解器结合，提供一定程度的交互性，使得用户可以实际参与到游戏求解过程中。设计中参考了多本专业书籍，如张健的《逻辑公式的可满足性判定》以及Tanbir Ahmed的硕士论文，这些资源为理论基础和算法实现提供了重要的支持。 这个项目不仅锻炼了学生的编程技能，还深入理解了SAT问题在实际问题中的应用，以及如何通过算法优化提升程序性能。通过这次课程设计，学生不仅掌握了DPLL算法的应用，还提高了分析复杂问题并寻求解决策略的能力。