目 录
1引言 1
1.1 课题背景与意义 1
1.2 国内外研究现状 1
1.3 课程设计的主要研究工作 1
2 系统需求分析与总体设计 1
2.1 系统需求分析 2
2.2 系统总体设计 2
3 系统详细设计 3
3.1 有关数据结构的定义 3
3.2 主要算法设计 4
4.系统实现与测试 11
4.1 系统实现 11
4.2 系统测试 19
4.3程序优化 23
5 总结与展望 24
5.1 全文总结 25
5.1 工作展望 25
6体会 26
附录 27
1. 主程序 27
2. 文件操作 31
3. SAT求解，DPLL算法核心框架 32
4. 数独求解模块 51
1引言
1.1 课题背景与意义
可满足性问题一直是人工智能领域研究的一个核心问题，其应用范围，不仅仅在人工智能，还包括计算机辅助设计，机器视觉，数据库等。合取范式的可满足性问题是理论计算机科学与人工智能的著名问题，寻求其有效算法，一直是计算机连及实际应用的重要任务。
本文简单的实现了基于DPLL的SAT算法，采用邻接表的数据结构和最短正字句的决策方式，并将算法应用在数独问题的求解过程中。
1.2 国内外研究现状
多年来，国际上已提出各种不同的局部搜索算法和回溯算法，使得S不同领域中SAT问题的解决能力增强，国际上提出的一大批采用回溯算法基本都是在DPLL回溯算法上，在变量决策，推理回溯等方面的优化。
在可满足问题研究的突破性进展，使得直接或者间接的推动人工智能等领域的突破性进展。目前SAT求解器可以高效地处理数百万变量规模的问题。然而,由于SAT问题本身的特性,除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解算法，因此设计出高度的SAT求解算法仍然是今天研究的热点。
1.3 课程设计的主要研究工作
DPLL算法是经典的SAT完备型求解算法，对给定的一个SAT问题实例，理论上可判定其是否满足，满足时可给出对应的一组解。本设计基于DPLL的算法与程序框架，实现一个完备SAT求解器，包括程序的改进也必须在此算法的基础上进行，对输入的CNF范式算例文件，解析并建立其内部表示；精心设计问题中变元、文字、子句、公式等有效的物理存储结构以及一定的分支变元处理策略，使求解器具有优化的执行性能；对一定规模的算例能有效求解，输出与文件保存求解结果，统计求解时间。
