基于DPLL算法的数独求解优化：理论与实践

本篇课程设计报告由计算机1705班学生王明明（学号U201714726）在2019年3月20日完成，指导教师为李丹，主要围绕"基于SAT的数独游戏求解程序"展开。论文的焦点在于对 Davis 和 Putnam 在1960年提出的DPLL（戴维斯-普特南算法）进行深入研究和优化，以解决数独游戏中的可满足性问题，这是一个典型的NP完全问题。 首先，作者介绍了SAT问题的基本概念，它是命题逻辑公式是否可满足的问题，有广泛的应用价值，特别是在硬件设计和安全协议验证等领域。设计目标是基于DPLL算法构建一个完备的SAT求解器，能够处理输入的CNF范式算例，通过设计合理的数据结构和分支策略来优化算法执行效率。 在系统设计部分，常量和变量被清晰定义，涉及的关键函数如公式解析、存储结构（如子句、公式等的物理表示）和DPLL算法核心思想都被详细阐述。作者提出了对原始DPLL算法的改进思路，旨在提升求解速度和准确性。 报告还包含对具体算例的测试，包括CNF算例和数独游戏实例。通过这些案例，作者分析了算法的性能，并讨论了优化前后算法的表现。设计还考虑了时间性能的测量，通过time.h库记录DPLL算法的执行时间，输出结果时包含这一信息。 此外，报告总结了整个设计过程中的感悟和收获，对指导教师和参考资料表达了感谢，并提供了源代码（main.c、SAT.h、satSolve.c、Sudoku.h、Game.c）以及相关的附录，以供读者深入了解和研究。 这篇报告深入探讨了DPLL算法在数独游戏求解中的应用，展示了如何通过优化算法和数据结构来提高求解效率，同时强调了理论与实践相结合的重要性。