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

本项目是李响在2020年春季进行的CS1802课程设计，主题是"基于SAT的二进制数独游戏求解程序"。该设计的核心内容是利用DPLL（Davis-Putnam-Logemann-Loveland）算法来解决SAT（可满足性问题）问题，这在计算机科学和人工智能领域具有重要地位，尤其在硬件设计和安全协议验证等领域有广泛应用。 DPLL算法是求解CNF（conjunctive normal form，析取范式）形式的逻辑公式是否可满足的关键算法。学生需要首先学习和掌握DPLL的基本原理，包括选择词策略、数据结构设计，如如何高效地存储变量、符号和子句，以提高算法的执行效率。同时，他们需要实现这个算法，并针对特定的输入CNF文件，解析其结构，构建相应的内部表示。 设计中还包括对输入输出功能的要求，确保程序可以接收用户输入的参数，读取并处理SAT算例文件，同时输出结果并将其保存到文件中。此外，还需要设计公式解析与验证模块，确保程序能够正确解析文件内容并能人工验证解析结果的准确性。 性能优化是设计的关键部分，学生需要对基本DPLL算法进行某一方面的优化，如改进存储结构或分支变元选取策略，通过对比优化前后的执行时间来计算优化率。通过这种方式，可以提升求解器在大规模实例上的处理速度。 项目进一步扩展到了实际应用，将二进制数独问题转换为SAT问题，集成到求解器中，使得用户可以交互式地体验数独游戏，同时展示SAT求解技术在解决这类问题中的实用性。这个过程需要参考相关文献，如张健的《逻辑公式的可满足性判定》和Tanbir Ahmed的DPLL算法实现。 李响的课程设计不仅涉及了基础的SAT求解算法实现，还包含了实际问题的转化、性能优化和用户体验设计，是一次结合理论与实践的综合性项目。