课程设计报告
题目：基于 SAT 的二进制数独游戏求解程序
计算机科学与技术学院
I
任务书
1.设计内容
SAT 问题即命题逻辑公式的可满足性问题（satisfiability problem），是
计算机科学与人工智能基本问题，是一个典型的 NP 完全问题，可广泛应用于许
多实际问题如硬件设计、安全协议验证等，具有重要理论意义与应用价值。本设
计要求基于 DPLL 算法实现一个完备 SAT 求解器，对输入的 CNF 范式算例文件，
解析并建立其内部表示；精心设计问题中变元、文字、子句、公式等有效的物理
存储结构以及一定的分支变元处理策略，使求解器具有优化的执行性能；对一定
规模的算例能有效求解，输出与文件保存求解结果，统计求解时间。
2.设计要求
要求具有如下功能：
⑴ 输入输出功能：包括程序执行参数的输入，SAT 算例 cnf 文件的读取，
执行结果的输出与文件保存等。
⑵ 公式解析与验证：读取 cnf 算例文件，解析文件，基于一定的物理结构，
建立公式的内部表示；并实现对解析正确性的验证功能，即遍历内部结
构逐行输出与显示每个子句，与输入算例对比可人工判断解析功能的正
确性。
⑶ DPLL 过程：基于 DPLL 算法框架，实现 SAT 算例的求解。
⑷ 时间性能的测量：基于相应的时间处理函数（参考 time.h），记录 DPLL
过程执行时间（以毫秒为单位），并作为输出信息的一部分。
⑸ 程序优化：对基本 DPLL 的实现进行存储结构、分支变元选取策略
[1-3]
等
某一方面进行优化设计与实现，提供较明确的性能优化率结果。优化率
的计算公式为：[(t-t
o
)/t]*100%,其中 t 为未对 DPLL 优化时求解基准算
II
例的执行时间，t
o
则为优化 DPLL 实现时求解同一算例的执行时间。
⑹ SAT 应用：将二进制数独游戏
[5，6]
问题转化为 SAT 问题
[6]
，并集成到上
面的求解器进行问题求解，游戏可玩，具有一定的/简单的交互性。
3.参考文献
[1] 张健著. 逻辑公式的可满足性判定—方法、工具及应用. 科学出版社，2000
[2]TanbirAhmed.An Implementation of the DPLL
Algorithm.Masterthesis,Concordia University,Canada,2009
[3] 陈稳. 基于 DPLL 的 SAT 算法的研究与应用.硕士学位论文，电子科技大学，
2011
[4]CarstenSinz.Visualizing SAT Instances and Runsof the DPLL
Algorithm.JAutom Reasoning (2007) 39:219–243
[5] Binary Puzzle：http://www.binarypuzzle.com/
[6] Putranto H. Utomo and Rusydi H. Makarim. Solving a Binary Puzzle.
Mathematics in Computer Science,(2017) 11:515–526
[7] Tjark Weber. A sat-based sudoku solver. In 12th International
Conference on Logic forProgramming, Artificial Intelligence and
Reasoning, LPAR 2005, pages 11–15, 2005.
[8]InsLynce and JolOuaknine. Sudoku as a sat problem.In Proceedings of
the 9th InternationalSymposium on Artificial Intelligence and
Mathematics, AIMATH 2006, Fort Lauderdale.Springer,2006.
[9] Uwe Pfeiffer, Tomas Karnagel and Guido Scheffler.A Sudoku-Solver for
Large Puzzles using SAT. LPAR-17-short (EPiC Series, vol. 13), 52–57
[10] Sudoku Puzzles Generating: from Easy to Evil.
http://zhangroup.aporc.org/images/files/Paper_3485.pdf
III
目录
任务书 .........................................................I
1.设计内容 .................................................I
2.设计要求 .................................................I
3.参考文献 ................................................II
基于 SAT 的二进制数独游戏求解程序 ...............................1
1 问题概述 .................................................1
2 DPLL 算法思想 .............................................2
3 功能要求 .................................................3
4 系统设计 ..................................................4
4.1 数据物理结构 ........................................4
4.2 演示系统 ...........................................4
4.3 cnf 文件读取和解析实现算法 ..........................5
4.4 二进制数独游戏实现算法 .............................8
5 系统实现 .................................................9
5.1 实验环境 ...........................................9
5.2 系统演示 ...........................................9
5.3 系统测试 ..........................................10
6 实验小结 ................................................13
附录 程序源代码 ...............................................15
1
基于 SAT 的二进制数独游戏求解程序
1 问题概述
SAT问题即命题逻辑公式的可满足性问题（satisfiability problem），是
计算机科学与人工智能基本问题，是一个典型的NP完全问题，可广泛应用于许多
实际问题如硬件设计、安全协议验证等，具有重要理论意义与应用价值。SAT问
题也是程序设计与竞赛的经典问题。
对于任一布尔变元x，x与其非“¬x”称为文字(literal)。对于多个布尔变元，
若干个文字的或运算l
1
∨l
2
∨…∨l
k
称为子句(clause)。只含一个文字的子句称为单
子句。不含任何文字的子句称为空子句，常用符号□表示。子句所含文字越多，
越易满足，空子句不可满足。
SAT问题一般可描述为：给定布尔变元集合{x
1
, x
2
, ..., x
n
}以及相应的子句集合
{c
1
, c
2
, ..., c
m
}，对于合取范式（CNF范式）：
F
= c
1
∧c
2
∧...∧c
m
，判定是否存在
对每个布尔变元的一组真值赋值使
F
为真，当为真时（问题是可满足的，SAT），
输出对应的变元赋值（一组解）结果。
一个CNF公式也可以表示成子句集合的形式：S={c
1
,c
2
,...,c
m
}.
例如，由三个布尔变元a,b,c所形成的一个CNF公式（¬a∨b）∧（¬b∨c）,可
用集合表示为{¬a∨b,¬b∨c}，该公式是满足的，a=0, b=0,c=1是其一组解。
一个CNF SAT公式或算例的具体信息通常存储在一个.cnf文件中，下图2.1是
算例problem1.cnf文件前若干行的截图。
