基于DPLL算法实现的完备SAT求解器的数独求解程序 毕业论文+任务书+项目源码

---

目录

任务书

1.引言

1.1课题背景与意义

1.2国内外研究现状

1.3课程设计的主要研究工作 3

2.系统需求分析与总体设计 4

2.1系统需求分析 4

2.2系统总体设计 4

3.系统详细设计 6

3.1有关数据结构的定义 6

3.2主要算法设计 9

4.系统实现与测试

4.1系统实现

4.2系统测试 20

5.总结与展望

5.1全文总结

5.2工作展望

6.体会

参考文献

课题背景：

命题逻辑公式的可满足性问题（SAT）是数理逻辑、计算机科学、集成电路设计与验证和人工智能等领域中的核心问题，并且是第一个被证明出来的NP完全问题。

从1960年至今，SAT问题一直备受人们的关注，世界各国的研究人员在这方面都做了大量的工作，提出了许多求解算法。每年可满足性理论和应用方面的国际会议都会组织一次 SAT竞赛以求找到一组最快的SAT求解器，而且会详细展示一系列的高效求解器的性能。国内也经常会组织一些SAT竞赛及研讨会，这些都促进了SAT算法的飞速发展。尽管命题逻辑的可满足性问题理论研究已趋于成熟，但在SAT求解器被越来越多地应用到各种实际问题领域的今天，探寻解决SAT问题的高效算法仍然是一个吸引人并且极具挑战性的研究方向。