基于QT实现的数独游戏DPLL的SAT求解器目录1引言11.1课题背景与意义

目录
1引言1
1.1课题背景与意义1
1.2国内外研究现状1
1.3课程设计的主要研究工作2
【基于QT实现的数独游戏DPLL的SAT求解器】2系统需求分析与总体设计3
2.1系统需求分析3
2.1.1SAT求解器3
2.1.2数独游戏3
2.2系统总体设计3
2.2.1SAT求解器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.1CNF范式操作11
3.2.2DPLL算法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.1cnf文件29
4.1.2DPLL文件31
4.1.3Sudoku文件32
4.2系统测试32
4.2.1SAT求解器模块测试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求解器和数独游戏两个功能。