目  录
1   引言 1
1.1  课题背景与意义 1
1.2  国内外研究现状 1
1.3  课程设计的主要研究工作 2
2   系统需求分析与总体设计 3
2.1  系统需求分析 3
2.1.1  SAT求解器 3
2.1.2  数独游戏 3
2.2  系统总体设计 3
2.2.1  SAT求解器 3
2.1.2  数独游戏 4
3   系统详细设计 6
3.1 有关数据结构的定义 6
3.1.1  数据结构定义 6
3.1.2  数据结构关联 9
3.1.3  相关常量声明 10
3.2  主要算法设计 11
3.2.1  CNF范式操作 11
3.2.2  DPLL算法 18
3.2.3  数独生成算法 19
3.3  程序优化 24
3.3.1  结构优化 24
3.3.2  函数递归转非递归 24
3.3.3  文字选取策略的优化 25
3.3.4  程序优化结果测试 27
4   系统实现与测试 29
4.1  系统实现 29
4.1.1  cnf文件 29
4.1.2  DPLL文件 31
4.1.3  Sudoku文件 32
4.2  系统测试 32
4.2.1  SAT求解器模块测试 33
4.2.2  数独功能模块测试 42
5   总结与展望 49
5.1 全文总结 49
5.2 工作展望 49
6   体会 51
参考文献 52
附录 53
1 引言
1.1 课题背景与意义
对于计算机科学与技术、信息安全与物联网专业大二学生，在前三个学期已经学习了C语言程序设计、数据结构两门面向编程知识与技术的基础理论课，以及C语言程序设计实验、数据结构实验两门编程实践课程，不仅具有较为系统性的C语言、常用数据结构基本知识，而且具有初步的程序设计、数据抽象与建模、问题求解与算法设计的能力，奠定了进行复杂程序设计的知识基础。但两门实验课仍属于对基本编程模型与技术的验证性训练，而“综合程序设计”课程设计正是使大家从简单验证到综合应用，甚至在编程中实现智慧与风格升华的重要实践环节，为后续学习与进行计算机系统编程打下坚实的基础，让综合编程技能成为大家的固有能力与通向未来专业之门的钥匙。
1.2 国内外研究现状
近十多年来，可满足性问题研究逐渐升温，已成为了国际国内的研究热点， 取得了一批相当重要的理论和实践成果，应该说当前的SAT问题研究比十多年前 已取得了很大的突破，并直接或间接地推动了其他相关领域（比如形式验证，人 工智能等领域）的发展。
国际上已提出了各种不同的局部搜索算法和回溯搜索算法，使得SAT解决器解决不同领域中的SAT问题的能力不断增强，能解决的问题的规模不断增大。其中局部搜索算法显示出对于随机的SAT问题特别有用，而回溯搜索算法则 被用来解决大规模实际应用领域中的SAT问题。事实上，国际上已提出了一大批 采用回溯搜索算法的高效的SAT问题解决器，其中绝大多数提出来的回溯搜索算 法是对原始的DPLL回溯搜索算法的改进算法。这些改进措施包括:新的 变量决策策略，新的搜索空间剪除技术，新的推理和回溯技术以及新的更快的算 法实现方案和数据结构等。当前水平的SAT问题求解器已能够轻松解决以前传统 SAT问题解决器完全无法解决的可满足性问题。
尽管当前的SAT问题解决器已取得了相当重要的进步，但是研究的脚步不会停止，我们还可以提出一些值得研究的问题。比如，是否存在新的更高效的SAT 问题处理技术可以集成到DPLL算法框架内；是否可以找到除局部搜索，回溯搜 索之外的其他SAT算法来更有效地解决SAT问题；是否能提出更好的SAT改进算 法和实现方案。
1.3 课程设计的主要研究工作
本次实验中，实验者选择了 “基于SAT的数独游戏求解程序”作为实验课题，实现SAT求解器和数独游戏两个功能。
SAT求解器基于DPLL的完备算法，对CNF范式算例文件进行求解，输出答案，并可选择遍历验证答案或将答案存入文件；数独游戏可转化为SAT问题，用本系统实现的SAT求解器可以快捷地对数独问题转化的CNF文件进行求解，再以变元真值数据转化的数独盘格式输出求解答案。本系统具有一定的交互功能，用户可以利用本系统进行数独游戏，系统将自动判断解的正确性，并输出正确答案。