基于DPLL算法实现的完备SAT求解器

Jonesy

发布日期: 2021-04-06 07:40:13 浏览量: 240
评分:
star star star star star star star star star star_border
*转载请注明来自write-bug.com

一、设计内容

SAT问题即命题逻辑公式的可满足性问题(satisfiability problem),是计算机科学与人工智能基本问题,是一个典型的NP完全问题,可广泛应用于许多实际问题如硬件设计、安全协议验证等,具有重要理论意义与应用价值。本设计要求基于DPLL算法实现一个完备SAT求解器,对输入的CNF范式算例文件,解析并建立其内部表示;精心设计问题中变元、文字、子句、公式等有效的物理存储结构以及一定的分支变元处理策略,使求解器具有优化的执行性能;对一定规模的算例能有效求解,输出与文件保存求解结果,统计求解时间。

设计要求

要求具有如下功能:

  • 输入输出功能:包括程序执行参数的输入,SAT算例cnf文件的读取,执行结果的输出与文件保存等

  • 公式解析与验证:读取cnf算例文件,解析文件,基于一定的物理结构,建立公式的内部表示;并实现对解析正确性的验证功能,即遍历内部结构逐行输出与显示每个子句,与输入算例对比可人工判断解析功能的正确性。数据结构的设计可参考文献

  • DPLL过程:基于DPLL算法框架,实现SAT算例的求解

  • 时间性能的测量:基于相应的时间处理函数(参考time.h),记录DPLL过程执行时间(以毫秒为单位),并作为输出信息的一部分

  • 程序优化:对基本DPLL的实现进行存储结构、分支变元选取策略[1-3]等某一方面进行优化设计与实现,提供较明确的性能优化率结果。优化率的计算公式为:[(t-to)/t]*100%,其中t 为未对DPLL优化时求解基准算例的执行时间,to则为优化DPLL实现时求解同一算例的执行时间

  • SAT应用:将数独游戏[5]问题转化为SAT问题[6-8],并集成到上面的求解器进行问题求解,游戏可玩,具有一定的/简单的交互性。应用问题归约为SAT问题的具体方法可参考文献[3]与[6-8]

1.引言

1.1 课题背景与意义

课题背景

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

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

研究意义

可满足性问题是计算机科学领域和人工智能等领域中的重要研究对象。但是 其求解算法的时间开销和空间开销却异常惊人。对于一个含有n个命题逻辑变量的合取范式来说,如果使用穷举法来罗列所有真值指派进行求解,虽然在理论上是可行的,但算法的时间复杂度却是为O(2n)级的,计算机如果采用这种方式进行求解将负担不起如此大的开销。

SAT问题为NP完全问题,NP完全问题排在七大数学难题之首,在计算复杂性理论中具有非常重要的地位,一方面因为它有着极大的理论价值并且非常难解,另一方面是一旦被破解以后,在诸多的工程领域里还可以得到广泛的应用。由于SAT问题是NP完全问题,它如果能够得到高效解决,那么一定可以高效地解决所有其它NP完全问题,这是因为所有的NP完全问题都能在多项式时间内进行相互转化,即所有的NP完全问题都能够在多项式时间内转换为可满足性问题。

研究能够解决SAT问题的高效算法在理论上有着重要的意义。SAT问题的应用领域非常广泛,例如在数学研究和应用领域,它能用来解决旅行商(Traveling Salesman Problem,TSP)和逻辑算术问题;在计算机和人工智能(Artificial Intelligence)领域中,它能解决CSP(约束满足问题)问题、语义信息的处理和逻辑编程等问题;在计算机辅助设计领域中,它能很好的解决任务规划与设计、三维物体识别等问题。许多的实际问题如人工智能、积木世界规划问题、数据库检索、Job shop排工问题、超大规模集成电路设计和图着色都可转换为 SAT 问题进行求解。不仅如此,一些实际问题通常还具有一定的结构特性,可以据此来对具有某一类结构特性的实际应用问题进行求解,进而得到解决该类问题的一种通用解法

1.2 国内外研究现状

基于DPLL算法的完备性SAT求解器是此次任务关注的重点。DPLL算法是由Davis和Putnam 等人在1960年提出,其它的完备算法大都是在DPLL算法的基础上衍生出来的,是对DPLL算法的改进。S.A.Cook在1971年证明了SAT问题是NP完全问题,这削弱了许多学者研究SAT问题的兴趣,从而导致了SAT问题在很长的一段时间里都没有得到较好的重视,发展非常缓慢,研究成果较少。但是1996年以后,很多国家都相继举办了一些SAT竞赛和研讨会,这使得越来越多的人开始关注并研究SAT问题。SAT协会是目前推动SAT问题理论和应用进展的主要驱动力量,其Satlive网站随时更新SAT研究动态,发布了一系列有关会议、竞赛、技术报告、论文、图书等信息;每年举办一次SAT理论和应用国际学术会议,目前已召开16届;SAT国际竞赛始于2002年,每隔两年或一年举办,2016年成功举办了第10届,汇聚了大批优秀的SAT求解器,影响力很大。

冲突驱动子句学习(Conflict Driven Clause Learning,简称CDCL)算法主要框架基于DPLL,是目前最重要的SAT求解算法,在冲突分析与子句学习、非时许回溯、重启、数据结构等方面做了一系列改进。当前代表性的CDCL求解器包括GRASP、Chaff、MiniSAT、Lingeling、Glucose、Sparrow等。其中Moskewicz等人提出的Chaff算法集合了laziness、线性学习和一系列启发式策略,强调“快速和低廉”的低负荷决策方法,是SAT问题求解算法的重要突破,形成流行求解器的相关思想。Lingeling、Glucose、Sparrow等近年来在SAT国际竞赛中屡获佳绩。国内也涌现出了许多高效的求解算法,如1998年作者梁东敏提出了改进的子句加权WSAT算法,2000年金人超和黄文奇提出的并行Solar算法,2002 年作者张德富在文献中,提出模拟退火算法。

尽管SAT算法已经取得了举足轻重的改进,但是仍有一些问题没有得到高效的解决,已经解决的问题可能还存在更好的求解算法,因此研究并实现高效率的求解算法仍是当前要解决的中心问题之一。

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

  • 对SAT问题的研究背景、意义及现状进行了简要总结,学习了命题逻辑可满足性问题的基本理论知识

  • 基于DPLL算法实现一个完备性的SAT问题求解器,能够用来求解一定规模的SAT问题

  • 对实现的SAT求解器进行优化,提高效率,改善其时间复杂度,从而用更少的时间求解更大规模的SAT问题

  • 将数独求解问题转换成SAT问题,并基于实现的SAT求解器编写一个数独求解程序

  • 基于数独求解程序开发出一个可以随机生成数独并具有一定可玩性的数独游戏

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

2.1 系统需求分析

  • 输入输出功能:包括程序执行参数的输入,SAT算例cnf文件的读取,执行结果的输出与文件保存等

  • 公式解析与验证:读取cnf算例文件,解析文件,基于一定的物理结构,建立公式的内部表示;并实现对解析正确性的验证功能,即遍历内部结构逐行输出与显示每个子句

  • DPLL过程:基于DPLL算法框架,实现SAT算例的求解

  • 时间性能的测量:基于相应的时间处理函数,记录DPLL过程执行时间(以毫秒为单位),并作为输出信息的一部分

  • SAT应用:将数独游戏问题转化为SAT问题,并集成到上面的求解器进行问题求解,游戏可玩,具有一定的/简单的交互性

2.2 系统总体设计

该系统共包括交互模块,SAT模块和数独模块:

  • 交互模块:显示交互环境,读取用户输入,显示执行结果

  • SAT模块:SAT模块由以下子模块组成:

    • CNF解析模块:该模块从文件中读取算例,进行解析,建立公式的内部存储,用于DPLL算法求解
    • DPLL算法模块:该模块使用DPLL算法对算例进行求解
    • 结果验证模块:该模块负责验证得出的解是否正确
    • 数独模块:数独模块由以下子模块组成:
      • 数独生成模块:该模块负责生成一个随机的数独
      • 数独转换模块:该模块负责将数独转换成SAT问题,保存到CNF文件中
      • 数独求解模块:该模块负责调用SAT模块对上一个模块生成的CNF文件求解,并将解转换为数独形式显示出来

模块结构图如图2-1所示:

3.系统详细设计

3.1 有关数据结构的定义

系统主要需要存储的有文字类型,子句类型,和公式类型,首先需要为这些类型选择合适的存储结构,为了便于删除和添加,系统中所用的数据结构基于邻接表结构,但又有所不同。

所用的数据结构类型

  • Variable类型:该数据结构包含指向前驱和后继结点的指针,构成双向链表,还有一个指向所在Clause的指针,和一个int型变量存储文字

  • Clause类型:该数据结构同样包含指向前驱和后继结点的指针,构成双向链表,还有一个Variable的指针指向Variable链表的头结点,还有一个int变量存储该子句剩余文字个数,还有一个int变量标记子句是否被删除的和一个int变量,用来记录子句因为哪个文字而删除

  • ClauseNode类型:该类型包含一个Clause结点的指针和一个指向后继结点的指针,构成单向链表,该链表的作用是将某一个文字出现过的所有子句链接起来

  • VariableNode类型:该类型包含一个Variable结点的指针和一个指向后继结点的指针,构成单向链表,该链表的作用是将某一个文字的反文字结点链接起来

  • RelativeChain类型:该类型包含一个int型变量标志当前文字是否已被删除,还包含一个ClauseNode结点的指针指向ClauseNode链表的头结点,还包含一个VariableNode结点的指针指向VariableNode链表的头结点

  • Formula类型:该类型包含一个int型变量记录变量个数,包含另一个int类型记录空子句个数,包含一个Clause的指针指向Clause链表的头结点,还包含一个动态分配的RelativeChain类型的数组

每个数据结构类型所含的数据项

Variable结构所含数据项如表3-1所示:

数据项名称 数据项类型 数据项作用
var int 存储文字的值
prior Variable * 指向前驱结点
next Variable * 指向后继结点
clause Clause * 指向所在子句

Clause结构所含数据项如表3-2所示:

数据项名称 数据项类型 数据项作用
varNumber int 存储该子句剩余文字个数
prior Clause * 指向前驱结点
next Clause * 指向后继结点
headVar Variable * 指向文字链表的头结点
isDeleted int 标记该子句是否已被删除
isDeletedBy Int 标记该子句因哪个文字被删除

ClauseNode结构所含数据项如表3-3所示:

数据项名称 数据项类型 数据项作用
clause Clause * 指向包含某文字的Clause结点
next ClauseNode * 指向后继结点

VariableNode结构所含数据项如表3-4所示:

数据项名称 数据项类型 数据项作用
variable Variable * 指向某文字的反文字结点
next VariableNode * 指向后继结点

RelativeChain结构所含数据项如表3-5所示:

数据项名称 数据项类型 数据项作用
isDeleted int 标记某文字是否已被删除
headClauseNode ClauseNode * 指向ClauseNode链表的头结点
headVariableNode VariableNode * 指向VariableNode链表的头结点

Formula结构所含数据项如表3-6所示:

数据项名称 数据项类型 数据项作用
varNumber int 存储变元个数
emptyClauseNumber int 指向存储空子句的个数
headClause Clause * 指向Clause链表的头结点
relativeChainArray RelativeChain * RelativeChain类型的数组

各数据结构之间的关联

各数据结构之间的关联如图3-1所示:

3.2 主要算法设计

本系统中的主要算法有以下三个:

3.2.1 DPLL算法

DPLL算法主要基于单子句传播策略和分裂策略。

单子句策略:若子句集中有一个单子句L,那么L一定取真值,于是可以从子句集中删除所有包含L的子句。若此时子句集变为空集,则该公式可满足;否则删除所有文字¬L,若此时子句集中含有空子句则公式不可满足,否则继续进行单子句传播策略。当没有单子句时进行分裂策略。

分裂策略:可以通过某种规则选取一个文字L,在子句集中添加一个单子句L,然后进行单子句传播策略。

其主要流程如图3-2所示:

3.2.2 随机生成数独算法

该算法主要思想是先随机生成一个终盘,再用挖洞法挖去某些格子,从而生成数独,每挖掉一个格子就调用修改的DPLL算法进行求解,确保始终只有唯一解。修改的DPLL算法作用是求出命题公式解的个数。与之前相比,不同之处在于当子句集为空时并不直接返回TRUE,而是将一个计数器加一后回溯,最后回溯到顶端时返回计数器。随机生成终盘的方法是用随机数填满左上、中间、右下三个九宫格,然后对这个不完整的终盘求解得出完整的终盘。当挖掉某一个格子之后数独不再只有唯一解时就将最后挖掉的格子填上,然后结束生成过程。

其主要流程如图3-3所示:

3.2.3 数独转换为SAT问题的算法

该算法用一个三维坐标(x,y,v)代表坐标为(x,y)的格子内的数为v,(x,y,v)用变量k=81*x+9*y+v表示,k为真即代表格子(x,y)的值为v,为假即代表格子(x,y)的值不为v。然后根据数独的特点对这些变元进行约束,首先对一个格子本身约束,任意x、y,(x,y,1)~(x,y,9)有且只有一个为真,即其中任意两个不同时为真,但9个变元析取应为真。然后对一行进行约束,即对任意x、v,(x,1,v)~(x,9,v)中只有一个为真,即其中任意两个不能同时为真。再对一列进行约束,同上;最后对一个九宫格进行约束,即确保任意一个九宫格内的九个数两两不同。最后,还可以根据已知的提示数对上述操作进行优化,避免一些多余的子句。

其主要流程如图3-4所示:

4.系统实现与测试

4.1 系统实现

编程环境:Microsoft Visual Studio 2017 version 15.9.1

注:源码中有平台相关的部分,只适用于Windows。

数据结构的C语言定义:

  1. //前置声明,解决Clause和Variable互相包含对方指针类型的环形依赖问题
  2. struct Clause;
  3. //文字的存储类型,以双向链表存储,便于删除和恢复,var为实际文字值。
  4. typedef struct Variable {
  5. int var;
  6. struct Variable *prior;
  7. struct Variable *next;
  8. struct Clause *clause;
  9. } Variable;
  10. /* 子句的存储类型,子句链表也是双向链表,其中包含一个文字链表的头结点,还包含两个标志位,一个标志该子句是否已被删除,另一个标志该子句是在删除哪个变量时被删除掉,用于回溯。 */
  11. typedef struct Clause {
  12. struct Clause *prior;
  13. struct Clause *next;
  14. Variable *headVar;
  15. int varNumber;
  16. int isDeleted;
  17. int isDeletedBy;
  18. } Clause;
  19. //关联子句链表的结点,关联子句链表为单链表,每个结点包含一个指向某个子句的指针。
  20. typedef struct ClauseNode {
  21. Clause *clause;
  22. struct ClauseNode * next;
  23. } ClauseNode;
  24. //关联文字链表的结点,关联文字链表也为单链表,每个结点包含一个指向某个文字的指针。
  25. typedef struct VariableNode {
  26. Variable *variable;
  27. struct VariableNode *next;
  28. } VariableNode;
  29. /* 关联链表,一个表示该文字是否已被删除的标志位,包含一个指向关联子句链表的头结点的指针和一个指向关联文字链表的头结点的指针。 */
  30. typedef struct RelativeChain {
  31. int isDeleted;
  32. ClauseNode *headClauseNode;
  33. VariableNode *headVariableNode;
  34. } RelativeChain;
  35. /* 公式的存储结构,varNUmber统计变量个数,clauseNumber统计子句个数,emptyClauseNumber统计空子句的个数,避免每次都要遍历结构来判断是否有空子句,还包含一个指向子句链表头结点的指针,还包含一个动态分配的关联链表数组。 */
  36. typedef struct Formula {
  37. int varNumber;
  38. int emptyClauseNumber;
  39. Clause *headClause;
  40. RelativeChain *relativeChainArray;
  41. } Formula;

该数据结构的优点主要有以下几点

  • 每一个文字都有与之相关联的子句和反文字链表,这样删除文字所在子句和文字时不需遍历子句集,可以直接定位目标

  • 该结构以非递归形式执行DPLL算法,省去了递归过程中每次都要复制公式和销毁公式的开销,且非递归效率要高于递归

  • 该结构维护一个变量标记当前子句集中的空子句个数,大于0即代表有空子句,从而避免每次都要遍历子句集来判断是否有空子句的开销

  • 该结构每次删除单子句或反文字时都是从邻接表中移除,但并不从关联链表中移除,这样可以很方便的进行回溯,空间占用也能始终保持不变

交互模块实现

该模块首先打印主界面,显示功能菜单,接受用户输入的选项。然后将输入转化合适的参数,调用适当的模块提供功能,并负责输出提示信息。

SAT模块实现

CNF解析模块

该模块注意要包含两个函数,一个从文件中读取公式,并将其存储到数据结构中,另一个从存储结构中读取将其以公式的形式显示出来。

  1. Formula * CreateFormula(char *fileName);

该函数接受一个文件名作为参数,读取指定cnf文件内容,并建立起公式的内部表示,将其存储到数据结构中。

  1. void ParseCnfFile(char *fileName);

该函数接受一个文件名为参数,首先调用CreateFormula函数建立起文件中公式的内部存储,再将其以命题公式的形式打印出来。

DPLL算法模块

该模块主要包括8个函数,一个负责删除决策变量,一个负责回溯时恢复被删除的决策变量,一个判断子句集是否为空,一个判断是否有空子句,一个进行BCP(布尔约束传播过程),一个负责选取决策变量,一个负责结束时销毁公式,最后一个为DPLL算法本身,负责初始化和逻辑部分,调用上述7个函数进行求解。

  1. void RemoveVariable(Formula *formula, int unitClause);

该函数删除一个文字,接受两个参数,第一个参数formula为创建的公式,unitClause为单子句文字,该函数的作用即从邻接表移除所有含有unitClause的子句,并将所有-unitClause文字结点移除。因为从关联链表就可以直接定位目标子句和文字结点,因此不需遍历整个子句集,效率有所提高。

  1. void RecoverVariable(Formula *formula, int unitClause);

该函数恢复一个被删除的文字,接受两个参数,第一个参数为创建的公式,unitClause为要恢复的文字,被删除的子句和文字结点通过关联链表进行访问,并将其重新插入到子句链表和文字链表中,且能保持位置不变。

  1. int IsEmptyFormula(Formula *formula);

该函数判断子句集是否为空,接受一个参数,formula为创建的公式,该函数简单的判断下子句链表中头结点的后继结点是否为NULL,若是则代表子句集已为空,返回1;否则返回0。

  1. int HasEmptyClause(Formula *formula);

该函数判断是否有空子句,接受一个参数,formula为创建的公式,formula有一个成员变量emptyClauseNumber,该变量记录空子句的数量,在每次删除和回溯文字时都进行维护,该函数简单判断formula->emptyClauseNumber是否大于0,若大于0代表有空子句,返回1;否则返回0。

  1. int BCP(Formula *formula, int pos, int *solution, int *isFlipped);

该函数进行BCP过程,接受四个参数,第一个参数formula为创建的公式,第二个参数pos为当前已决策的变元的个数,solution即为记录已决策变元的数组,isFlipped数组标记已决策的变元中有哪些已经进行过反转,后两个参数在回溯时会用到。该函数首先扫描邻接表判断有没有单子句,若有则以formula和单子句文字为参数调用RemoveVariable函数,然后重新开始扫描,直到再没有单子句,并更新另外三个参数的值。

  1. int GetTarget(Formula *formula);

该函数作用是选取决策变量,该函数接受一个参数,formula为创建的公式,该函数使用MOM算法进行变量决策,该算法最重要的是求解出和文字L相对应的权值,最终选择权值最大的文字作为决策变量,权值为W(L)= ∑2-n,n为包含有文字L的每个子句的长度,将2的-n次幂求和,即为该文字的最终权值。该决策方法原理即为优先选择最短子句中的文字,这样能显著减少回溯次数,在求解不可解问题时优势很大。

  1. void DestroyFormula(Formula *formula);

该函数作用是当DPLL算法结束时负责销毁公式,释放内存。该函数首先销毁每一个文字链表,再销毁子句链表;然后遍历关联链表数组,销毁每一个关联链表,最后销毁关联链表数组,最终销毁公式结构。

  1. int DPLL(Formula *formula, int *solution);

该函数即为DPLL的主要逻辑函数,该函数负责初始化需要的内容和主要逻辑地实现,主要逻辑即先进行单子句传播过程,然后获取决策变量并删除,然后再次单子句传播过程。重复上述操作,当有空子句时进行回溯,子句集为空时返回1,代表已得出解并结束函数。

结果验证模块

  1. int test(Formula * formula, int * solution);

该函数的功能是验证得出的解是否正确。该函数接受两个参数,formula为创建的公式,solution为得出的解。该函数简单地根据得出的解对变元进行真值指派,然后判断该真值指派是否能使得公式为真。若能使公式为真则返回TRUE代表解正确;否则返回FALSE代表解错误。

数独模块实现

数独生成模块

  1. int DPLLPP(Formula *formula, int *solution);

该函数是修改后的DPLL算法,作用是求出一个cnf文件解的个数。该函数接受两个参数,formula为创建的公式,solution保存当前的解。该函数的不同之处在于当求出一个解之后并不立即返回,而是将解的个数递增,然后回溯,直到回溯到最顶层变量时才结束函数,返回解的个数。该函数用于确保生成的数独只有唯一解。

  1. int GetTargetPP(Formula *formula);

该函数为求解数独时所采用的变元决策方法。接受一个参数,formula为创建的公式。该函数简单选择第一个未决策的变元,并默认其为FALSE,较为贴近数独的实际情况,最后返回选出的决策变元。

  1. int TheSolutionOfSudoku(char sudoku[9][9]);

该函数的作用是求解数独的个数。该函数接受一个参数,即当前生成的数独。该函数首先调用数度转换模块将数独问题转化为cnf文件,然后调用DPLLPP函数求出cnf文件的解的个数,最后返回解的个数。

  1. char * CreateSudoku();

该函数的作用是生成一个随机的数独。首先用1-9的随机数填充数独中左上、中间、右下三个九宫格。然后调用数独求解模块对这个不完整的数独进行求解,得出一个终盘。接下来再随机挖去一个格子,调用TheSolutionOfSudoku函数检查数独是否是唯一解,若是则重复上述步骤;当不再只有唯一解时,将最后挖掉的格子还原,数独生成结束。返回一个一维数组用来存储数独。

数独转换模块

  1. void SudoToSat(char sudo[9][9]);

该函数的作用是将数独问题转换成cnf文件。接受一个参数,为生成或读入的数独,该函数首先用变元来表示数独,然后按照数独规则,对变元进行约束,将约束子句写入sudoku.cnf文件中。

  1. void SatToSudo(int *solution);

该函数的作用是将cnf文件的解转换成数独并打印出来。接受一个参数,该参数为DPLL算法求出的解,该函数根据每个变元的值构建出数独并显示出来。

数独求解模块

  1. void SolveSudoku(char sudoku[9][9]);

该函数的作用是求解生成的数独。接受一个参数,为生成或读入的数独。该函数首先调用SudoToSat函数将数独转换成cnf文件,然后调用SolveSat函数对生成的sudoku.cnf文件求解,并将解写入sudoku.res文件。然后调用SatToSudoku函数将得出的解转换成数独的形式并打印出来。

函数调用关系:各函数间的调用关系如图4-1所示,图中B指向A代表在A中调用B。

4.2 系统测试

为了增强程序的交互性和数独游戏的可玩性,使用Qt为所写程序设计了图形用户界面。

测试模块主要测试以下模块:

  • CNF解析模块:读取cnf文件并建立内部存储的模块

  • SAT模块:求解用cnf文件表示的sat问题的模块

  • 数独求解模块:给定数独对其进行求解的模块

  • 数独模块:随机自动生成可玩数独的模块

4.3 功能测试

4.3.1 CNF解析模块

测试方法为首先选择解析模块,然后随意选取一个cnf文件,观察输出结果。测试过程如图4-2、4-3所示。输出结果如图4-4所示。

首先选择解析模块

选择一个cnf文件

cnf文件解析结果

从图4-4中可以看到解析模块正确的输出了CNF文件的公式表示,说明解析模块功能正常,可以正确的建立公式的内部表示。

4.3.2 SAT模块

测试方法为首先选择解SAT问题模块,然后随意选取一个cnf文件,程序会对其进行求解,并在有解的情况下自动验证得出的解是否正确,若正确则将得出的解写入res文件中。测试过程如图4-5、4-6、4-7、4-8所示。最终得出的解如图4-9所示。

选择解SAT模块

选择一个cnf文件

得出解之后检验得出的解是否正确

将得出的解写入文件

结果

从图4-7验证模块的输出中可以看出SAT模块得出的解是正确的,图4-9中可以看出该模块将得出的解按照格式输出到了一个文件中,说明该模块功能正常。

4.3.3 数独求解模块

即给定数独对其进行求解的模块。

测试方法为首先选择解数独问题模块,然后输入数独进行求解,观察输出结果。测试过程如图4-10、4-11、4-12所示。输出结果如图4-13所示。

选择解数独问题模块

界面的提示信息

输入数独问题

解数独模块的输出结果

图4-12、4-13对比可以很明显的看出该模块正确的求解出了数独,该模块功能正常。

4.3.4 数独模块

测试方法为首先选择玩数独模块。然后可以填上空格,当结果正确时输出已完成的信息。测试过程如图4-14、4-15所示。完成时结果如图4-16所示。

选择玩数独模块

随机生成的数独

解出数独

从图4-15中可以看出程序正确的生成并输出了一个随机数独,从图4-16中可以看出程序正确的解出了生成的数独,该模块功能正常。

4.3.5 测试结果

对每个模块都进行多次上述测试,测试结果全部正确。可以得知每个模块都能很好地完成预定的任务,功能测试完成。

4.4 性能测试

性能测试主要测试SAT模块,为了体现出性能的变化,采用对比的方式进行测试。本程序记为程序1;另有程序2,程序2基于普通的邻接表数据结构和普通的递归结构,变量决策方法直接选取第一个还未决策的变量,使用DPLL算法进行求解。

测试数据:13个可满足的小型算例,10个可满足的中型算例,3个大型算例,6个不满足算例。共32个算例。测试时间上限为100秒。测试结果分别如表4-1、4-2、4-3、4-4所示。

小型算例测试结果

测例 变元数量 子句数量 程序1用时(ms) 程序2用时(ms) 优化率
problem1-20.cnf 20 91 <1 1 0
problem2-50.cnf 50 80 <1 140 100.00%
problem3-100.cnf 100 340 7 5153 99.86%
problem6-50.cnf 50 100 1 202 99.50%
problem8-50.cnf 50 300 1 5 80.00%
problem9-100.cnf 100 200 1 88844 100.00%
problem11-100.cnf 100 600 4 1834 99.78%
tst_v25_c100.cnf 25 100 <1 1 0
7cnf20_90000_90000_7.shuffled-20.cnf 20 1532 58 73 20.55%
ais6.cnf 61 581 1 3 66.67%
anomaly.cnf 48 261 1 3 66.67%
flat30-1.cnf 90 300 1 1 0
tst_v100_c400.cnf 100 400 1 4 75.00%

中型算例测试结果

测例 变元数量 子句数量 程序1用时(ms) 程序2用时(ms) 优化率
ais10.cnf 181 3151 592 952 37.82%
problem5-200.cnf 200 320 126 >100000 100.00%
problem12-200.cnf 200 1200 57 94747 99.94%
sud00012.cnf 232 1901 298 265 -12.45%
sud00079.cnf 301 2810 3841 4932 22.12%
sud00082.cnf 224 1762 587 823 28.68%
sud00861.cnf 297 2721 2073 1767 -17.31%
bart17.shuffled-231.cnf 231 1166 1 1 0
sw100-1.cnf 500 3100 18 73 75.34%
sw100-70.cnf 500 3100 74 9967 99.26%

大型算例测试结果

测例 变元数量 子句数量 程序1用时(ms) 程序2用时(ms) 优化率
bw_large.a.cnf 459 4675 55 1478 96.28%
eh-dp04s04.shuffled-1075.cnf 1075 3152 4974 >100000 100.00%
e-par32-3.shuffled-3176.cnf 3176 10297 >100000 >100000 0

不满足算例测试结果

测例 变元数量 子句数量 程序1用时(ms) 程序2用时(ms) 优化率
unsat-5cnf-30.cnf 30 420 20 101 80.20%
php-010-008.shuffled-as.sat05-1171.cnf 80 370 401 1301 69.18%
u-5cnf_3900_3900_060.shuffled-60.cnf 60 936 14611 >100000 100.00%
u-problem7-50.cnf 50 100 8 206 96.12%
u-problem10-100.cnf 100 200 18710 >100000 100.00%
tst_v50_c500.cnf 50 500 2 12 83.33%

由表格中的数据可以看出,除了个别算例之外,改进之后的求解器明显比改进之前高效了许多。小型算例的优化率基本都在50%以上;到了中型算例,优化率明显下降且有负优化迹象出现,但负优化的算例只占少数,且负优化率并不高,而正优化的算例优化率虽然明显下降,但还是占据着很大的优势;至于大型算例,因为能力有限,实现的求解器只能对较少的大型算例求解,因此测试算例较少,但可看出优化后的性能远高于优化前;最后是不可满足算例,因为不可满足算例的求解难度远高于可满足算例,因此只选取了其中六个算例作为测试,从中可以看到优化率均在60%以上,由此可知改进之后的求解器对不可满足算例的求解能力明显强于改进前。

测试结果

总体上分析可得,无论是可满足算例还是不可满足算例,优化之后的算法性能都明显优于优化前的算法,基本达到了性能优化的目的,性能测试完成。

5.总结与展望

5.1 全文总结

这次任务主要完成的工作如下:

  • 设计程序结构,划分模块,制定程序框架和流程

  • 实现各模块,分别调试各模块直至确保正确再进行下一个模块的实现

  • 将各模块组装起来,使之协调工作,拼接成一个整体

  • 设计交互,完善交互过程

  • 进行调试,改正代码中的错误和有可能导致错误的地方

  • 设计新的数据结构,改进算法,优化程序

  • 重新调试,确保解决所有错误

  • 完成工作

5.2 工作展望

在今后的研究中,围绕着如下几个方面开展工作:

  • 改进数据结构:从这次的工作中可以看出数据结构的选择对求解效率有很大的影响。而本次任务最终选择的数据结构仍然有很多的不足之处,有很多需要改进的地方,创造新的更加高效的数据结构是接下来研究的一个重点方向

  • 改进变量决策方法:变量决策方法可以说是DPLL算法中最重要的一环,如何快速的选择出最适合的变量是该算法中的一个核心问题,本次实验中改用MOM算法后可以看出算法速度明显上升,但MOM算法也有很多缺点,最大的缺点就是算法开销太大,因此,寻找或者创造新的更好的算法,是后续工作的主要方向

  • 各种辅助策略:例如子句学习,冲突导出等策略。虽然因为此次任务的时间并不充裕导致没有时间加入这些辅助策略。但毫无疑问这些策略对DPLL算法的效率同样有着非常大的影响

6.体会

本次任务是对数据结构课堂知识的一次全面回顾和总结。此次任务中,我收获巨大。首先,我体会到了模块化程序设计的完整过程;在此次任务中各模块相互独立,通过调用别的模块来提供服务,这一设计的优点主要体现在随后的优化过程中,在优化的过程中得益于模块化的设计思想,可以把工作重点集中在一小部分上,只对最影响效率进行优化,而不用把所有相关代码全部修改,这一点大大节省了优化过程的工作量。其次,本次实验加深了我对常见数据结构的理解和应用;我最初选择普通的邻接表作为数据结构,而DPLL算法需要实现删除、插入和遍历等操作,在实现这些功能的过程中我对临接表这些操作的实现有了更加深刻的认识,积累了丰富的经验,随后更是基于这些经验对普通邻接表结构进行了改进,创造出了自己的更适合DPLL算法的数据结构。最后,这次任务也让我完整的体会了一次程序从设计到实现再到优化最终完成的完整过程。设计部分力求程序结构清晰、模块功能明确,实现过程中逐模块实现、逐模块调试,直到确定一个模块完成并且正确时才继续下一个模块,最后优化过程中针对算法低效的部分进行优化;整个过程层次分明,可操作性强,最后易于差错和调试,是一次宝贵的经验。

本次实验中也遇到了很多的问题。最大的问题是在为新的数据结构编写DPLL算法时,因为考虑不周,错误的沿用了之前的销毁子句集函数,只是简单的对其进行扩充就直接使用了。后来发现这么做并不能真正的释放程序的空间,导致了严重的内存泄漏问题,发现问题之后企图进行改正,但发现因为数据结构本身的缺陷,无法在不回溯的情况下正确的释放程序的所有空间,因此不得不在释放空间之前,先把子句集回溯到初始的状态,然后再调用销毁函数进行销毁。这一问题反映出在设计的时候并没有做到全面考虑,从而导致了该问题,不过好在发现问题之后能够及时解决。

参考文献

[1] 陈稳. 基于DPLL的SAT算法的研究及应用. 2011.5

[2] 霍亚飞. Qt Createor快速入门 第三版. 北京航空航天大学出版社 2017.1

上传的附件 cloud_download 基于DPLL算法实现的完备SAT求解器.7z ( 4.21mb, 1次下载 )
error_outline 下载需要11点积分

发送私信

如果这世界上真有奇迹,那只是努力的另一个名字

15
文章数
11
评论数
最近文章
eject