基于SAT的对角线数独游戏求解程序

1.1 问题概述

SAT问题即命题逻辑公式的可满足性问题（satisfiability problem），是计算机科学与人工智能基本问题，是一个典型的NP完全问题，可广泛应用于许多实际问题如硬件设计、安全协议验证等，具有重要理论意义与应用价值。SAT问题也是程序设计与竞赛的经典问题。

对于任一布尔变元x，x与其非“¬x”称为文字(literal)。对于多个布尔变元，若干个文字的或运算l₁∨l₂∨…∨l_k称为子句(clause)。只含一个文字的子句称为单子句。不含任何文字的子句称为空子句，常用符号□表示。子句所含文字越多，越易满足，空子句不可满足。

SAT问题一般可描述为：给定布尔变元集合{x₁, x₂, ..., x_n}以及相应的子句集合{c₁, c₂, ..., c_m}，对于合取范式（CNF范式）：F = c₁∧c₂∧...∧c_m，判定是否存在对每个布尔变元的一组真值赋值使F为真，当为真时（问题是可满足的，SAT），输出对应的变元赋值（一组解）结果。

一个CNF公式也可以表示成子句集合的形式：S = {c₁, c₂, ..., c_m}.

例如，由三个布尔变元a, b, c所形成的一个CNF公式（¬a∨b）∧（¬b∨c）,可用集合表示为{¬a∨b, ¬b∨c}，该公式是满足的，a=0, b=0,c=1是其一组解。

一个CNF SAT公式或算例的具体信息通常存储在一个cnf 文件中，下图1.1是算例problem1.cnf文件前若干行的截图。

在每个CNF文件的开始，由‘c’开头的是若干注释说明行；‘p’开头的行说明公式的总体信息，包括：范式为CNF；公式有200个布尔变元，由1到200的整数表示；320个子句。之后每行对应一个子句，0为结束标记。46表示第46号变元，且为正文字；-46则是对应的负文字，文字之间以空格分隔。

DPLL算法是经典的SAT完备型求解算法，对给定的一个SAT问题实例，理论上可判定其是否满足，满足时可给出对应的一组解。本设计要求实现基于DPLL的算法与程序框架，包括程序的改进也必须在此算法的基础上进行。

1.2 DPLL算法思想

DPLL算法是基于树/二叉树的回溯搜索算法，主要使用两种基本处理策略：

单子句规则。如果子句集S中有一个单子句L,那么L一定取真值，于是可以从S中删除所有包含L的子句（包括单子句本身），得到子句集S₁，如果它是空集，则S可满足。否则对S₁中的每个子句，如果它包含文字¬L,则从该子句中去掉这个文字，这样可得到子句集合S₂。S可满足当且仅当S₂可满足。单子句传播策略就是反复利用单子句规则化简S的过程。

分裂策略。按某种策略选取一个文字L.如果L取真值，则根据单子句传播策略，可将S化成S₂；若L取假值（即¬L成立）时，S可化成S₁.

交错使用上述两种策略可不断地对公式化简，并最终达到终止状态，其执行过程可表示为一棵二叉搜索树,如下图1.2所示。

基于单子句传播与分裂策略的DPLL算法可以描述为一个如后所示的递归过程DPLL( S ), DPLL算法也可用非递归实现。

DPLL( S) :

/* S为公式对应的子句集。若其满足，返回TURE；否则返回FALSE. */

{

while(S中存在单子句) {//单子句传播

在S中选一个单子句L；

依据单子句规则，利用L化简S；

if S = Φ return(TRUE);

else if (S中有空子句 ) return（FALSE）；

}//while

基于某种策略选取变元v； //策略对DPLL性能影响很大

if DPLL（S ∪v ）return(TURE); //在第一分支中搜索

return DPLL(S ∪¬v);//回溯到对v执行分支策略的初态进入另一分支

}

对于公式{¬1∨2, ¬2，¬3∨4, 3∨¬5,3∨4, 3∨5，¬2∨¬5∨6} ,大家可以利用DPLL算法进行手动推理其搜索处理及回溯过程，获得求解结果。

1.3 功能要求

本设计要求精心设计问题中变元、文字、子句、公式等有效的物理存储结构，基于DPLL过程实现一个高效SAT求解器，对于给定的中小规模算例进行求解，输出求解结果，统计求解时间。要求具有如下功能：

1. 输入输出功能: 包括程序执行参数的输入，SAT算例cnf文件的读取，执行结果的输出与文件保存等。(15%)
2. 公式解析与验证: 读取cnf算例文件，解析文件，基于一定的物理结构，建立公式的内部表示；并实现对解析正确性的验证功能，即遍历内部结构逐行输出与显示每个子句，与输入算例对比可人工判断解析功能的正确性。数据结构的设计可参考文献[1-3]。(15%)
3. DPLL过程: 基于DPLL算法框架，实现SAT算例的求解（数据结构不要使用C++现有的vector等类库）。(35%)
4. 时间性能的测量: 基于相应的时间处理函数（参考time.h），记录DPLL过程执行时间（以毫秒为单位），并作为输出信息的一部分。(5%)
5. 程序优化: 对基本DPLL的实现进行存储结构、分支变元选取策略^[1-3]等某一方面进行优化设计与实现，提供明确的性能优化率结果。优化率的计算公式为：[(t-t_o)/t]*100%,其中t 为未对DPLL优化时求解基准算例的执行时间，t_o则为优化DPLL实现时求解同一算例的执行时间。(15%)

功能（1）至（5）为基础功能，占功能分值的85%。

6. SAT应用: 将对角线数独游戏^[12-13]问题转化为SAT问题^[6-8]，并集成到上面的求解器进行数独游戏求解，游戏可玩，具有一定的/简单的交互性。应用问题归约为SAT问题的具体方法可参考文献[3]与[6-8]。（15%）

1.4 实现与测试说明

1、普通数独游戏格局的生成与归约

普通数独游戏要求在9×9的网格中每个单元（cell）填入1至9的一个数字，必须满足三种约束：每一行、每一列及9个3×3的盒子中的数字都不重复。

一个数独游戏初始时已经提供了一些提示数，如图2.3中的左图，要求在剩下的空格中填满数字。初始游戏格局要求只有唯一解（一般至少要有17个提示数），基于推理可以求解。如何生成一个有效的数独游戏格局？一种方案可以从互联网或数独文件读取不少于50个不同的初始合法格局（此生成设计计分评定为良）；另一种方案是设计一种算法自动生成（此生成设计计分评定为优），一般可采用从完整合法填充开始，基于挖洞法生成^[9-11]。

本课程设计要求利用DPLL SAT求解算法对对角线数独游戏进行求解，因此首先必须理解如何将普通数独游戏转化（归约）为SAT问题，并把它表示为CNF公式的形式。这里要考虑三个问题：（1）如何定义问题的BOOL变元？（2）如何用CNF的子句集表示数独游戏的三种约束？（3）如何表示游戏格局中的提示数条件？下面分别给出一种方案供参考。

变元可按语义编码为1～9之间数字构成的三位整数ijk，i, j, k∈{1,2,…,9}，其中i表示单元格的行号，j表示单元格的列号，k表示单元格<i, j>填入的数字为k。如163变元表示第1行6列填入3；负文字 -452表示第4行5列不填入2。这样编码共有729个变元。

数独游戏的基本要求是：每个单元格只能填入1～9之间唯一一个数字，称之为“格约束”。以单元格<1,1>例，这可以表示为如下子句：

111 112 113 114 115 116 117 118 119 0

-111 -112 0

-111 -113 0

……

-118 -119 0

上述表示中，每个子句的末尾的0表示结束标记；第一个子句的含义是单元格<1,1>可填入至少一个数字；后面的子句集共同表示只能填入一个数字，子句-111 -112 0表示不能同时填1与2；其它类推。按这种方式需要对81个单元格进行类似表示，得到对应的子句集。

行约束要求每行需要填入1～9中的每个数字，且每个数字只出现一次。以第1行为例可表示为（此处在每个子句后加入注释，说明子句的含义）：

111 121 131 141 151 161 171 181 191 0 第1行含有1

112 122 132 142 152 162 172 182 192 0 第1行含有2

… …

119 129 139 149 159 169 179 189 199 0 第1行含有9

-111 -121 0 前两格不同时为1

-111 -131 0 第1与第3格不同时为1

… …

-111 -191 0 第1与第9格不同时为1

… …

列约束仿照行约束易于表示为对应子句集，同学们可自行写出。

对于3×3的盒子约束，以左上角的盒子为例进行说明，其子句集可表示如下：

111 121 131 211 221 231 311 321 331 0 包含1

112 122 132 212 222 232 312 322 332 0  包含2

… …

119 129 139 219 229 239 319 329 339 0 包含9

-111 -211 0 11格与21格不同时为1

-111 -311 0 11格与31格不同时为1

-111 -121 0 11格与12格不同时为1

… …

最后，对于每个具体的数独游戏，已经填入了部分提示数，如图2.3中的左图，每个提示数可表示为一个单子句，如第2行3列填入5，对应单子句如下：

235 0

SAT公式CNF文件中，一般变元是从1进行连续编码的，可以将上述语义编码转换为自然顺序编码，公式为：ijn → (i-1)*81+(j-1)*9+n；当按自然编码对数独游戏对应的CNF公式求解后，可设计逆变换公式将解解析为对应的游戏填充方案，完成填充，或给游戏玩家给予每一步填充的正误提示。

根据上面的分析，数独约束生成CNF子句集易于用多重循环结构实现^[6,8]。

2、对角线数独游戏的生成与CNF归约

对角线数独游戏^[12-13]是一种变型的数独，即在上述普通数独的基础上又增加了一类约束：对角线约束，如图1.4所示。对角线约束要求在两条对角线（撇对角线与捺对角线）上的数字也不能重复。

对角线数独游戏初始格局的生成也有两种类似的方案：（1）从互联网 http://www.sudoku-space.com/x-sudoku/ 或对角线数独文件读取不少于20个不同的初始合法格局（此生成设计计分评定为良）；（2）设计一种算法自动生成（此生成设计计分评定为优），采用从完整合法填充开始，基于挖洞法生成^[9-11]。

显然，将对角线数独游戏转化为SAT问题时，只需在普通数独游戏生成的子句集上补充对角线约束所生成的全部子句。根据语义编码方案，捺对角线上的9个格对应的位置编码分别为：11，22，33，44，55，66，77，88，99；而撇对角线上9个格的位置编码分别为：19，28，37，46，55，64，73，82，91。类似行约束可生成对角线约束的全部子句，请同学们自行设计对应转化生成算法。

3、程序主控流程

根据设计问题的功能要求，图2.5提供了一个程序处理流程图，红色部分为基于DPLL的SAT求解相关功能模块（课程设计首先必须完成的功能），蓝色部分是游戏生成、转化、求解等处理模块（求解必须调用DPLL SAT求解过程）。此流程图仅供参考，不限定同学们的设计，可以以此为参照自由发挥。

4、程序模块化

设计程序要求模块化，程序源代码进行模块化组织。主要模块包括如下：

（1）主控、交互与显示模块（display）；

（2）CNF解析模块（cnfparser）；

（3）核心DPLL模块( solver)；

（4）对角线数独模块，包括游戏格局生成、归约、求解(X-Sudoku)。

5、CNF公式的内部存储结构

本应用处理的主要数据对象有变元或文字、子句、公式等。同学们可以分析这些数据的逻辑关系及其施加的基本运算而建立相应的抽象数据类型，设计其物理存储结构。如子句有创建createClause、销毁destroyClause、增加addClause、删除removeClause、判断是否为单子句isUnitClause、评估子句的真假状态evaluateClause等运算。由于每个CNF公式变元与子句数可能不同，同一个实例中子句长度也可能不等,一种基本的处理方式是将子句表示为由文字构成的链表；整个公式则是由子句构成的链表，如图2.6所示，这里仅供参考（也许并非最优结构），同学们可自行设计相应的物理存储结构并进行优化,有效支持回溯。

6、测试算例要求(建议在内存≥8G的计算机上执行测试)

不少于18个SAT算例，其中可满足的算例不少于15个，不满足的算例不少于3个，大中小算例各占三分之一。鉴于大家实现的可能只是初级求解器，对算例规模的要求为：小型算例变元数为100个左右；中型算例变元数介于200-500个； 大型算例变元数600个以上。本设计提供部分cnf算例集,同学们可寻找与选择、扩充测试算例。在设计报告的测试分析部分列表给出每个测试算例下列信息：算例名、算例变元数、子句数与变元数比值、满足还是不满足或不确定、DPLL求解时间(t与t_o)以及优化率等信息。课堂检查时，主要对基准算例进行测试。

7、输出文件规范

对每个算例的求解结果要求输出到一个与算例同名的文件（文件扩展名为.res），文件内容与格式要求如下：

s 求解结果//1表示满足，0表示不满足，-1表示在限定时间内未完成求解

v -1 2 -3 … //满足时，每个变元的赋值序列，-1表示第一个变元1取假，2表示第二个变元取真，用空格分开，此处为示例。

t 17 //以毫秒为单位的DPLL执行时间，可增加分支规则执行次数信息

1.5参考文献

[1] 张健著. 逻辑公式的可满足性判定—方法、工具及应用. 科学出版社，2000

[2]Tanbir Ahmed. An Implementation of the DPLL Algorithm. Master thesis, Concordia University,Canada,2009

[3] 陈稳. 基于DPLL的SAT算法的研究与应用.硕士学位论文，电子科技大学，2011

[4]Carsten Sinz. Visualizing SAT Instances and Runs of the DPLL Algorithm. J Autom Reasoning, (2007) 39:219–243

[5]360百科：数独游戏https://baike.so.com/doc/3390505-3569059.html

[6] Tjark Weber. A sat-based sudoku solver. In 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2005:11–15

[7] Ins Lynce and Jol Ouaknine. Sudoku as a sat problem. In Proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics, AIMATH 2006.

[8] Uwe Pfeiffer, Tomas Karnagel and Guido Scheffler. A Sudoku-Solver for Large Puzzles using SAT. LPAR-17-short (EPiC Series, vol. 13): 52–57

[9] Sudoku Puzzles Generating: from Easy to Evil.

http://zhangroup.aporc.org/images/files/Paper_3485.pdf

[10] 薛源海，蒋彪彬，李永卓. 基于“挖洞”思想的数独游戏生成算法. 数学的实践与认识,2009,39(21):1-7

[11] 黄祖贤. 数独游戏的问题生成及求解算法优化. 安徽工业大学学报(自然科学版), 2015,32(2):187-191

[12] 对角线数独简介,

https://www.toutiao.com/article/7268970095840756224/?log\_from=c34b227a9af95\_1715086601212

[13] X-Sudoku online，http://www.sudoku-space.com/x-sudoku/