DPLL-Algorithm

An algorithm to solve SAT problem

1 系统总体设计

1.1 系统总流程

1.2 模块功能描述

1.Start模块：输出提示词，提示用户输入参数进行选择，输入1进入数独模块，输入2进入SAT问题模块。

2.CnfParser模块：读取后缀为.cnf的文件数据，将文件中的变元数和子句数提取出来保存，将每个子句保存入设定好的数据结构中，并将每个子句末尾的0丢弃。保存成功后，遍历输出结果人工与文件内容比对观察是否正确读取。

3.DPLLSolver模块：该模块主要实现DPLL算法框架，是本程序的核心框架。该算法计算cnf公式的变元真假值并将结果记录下来。若cnf文件中的算例有解的话，就会返回TRUE，将变元的结果输出；若算例无解返回FALSE，不输出结果。

4.Sudoku模块：该模块是数独模块。首先使用挖洞法生成数独终盘，再挖洞生成数独初盘。将数独初盘转化成SAT问题，即将其转换成CNF公式输入到.Cnf文件中，并将文件名返回main函数中。在经过CnfParser模块解析文件后，使用该模块中的SudokuDPLL函数计算出数独的结果并输出。

2 系统详细设计

2.1 数据结构定义

1）子句头节点定义：

typedef struct HeadNode {
    
    int Num = 0;
    
    DataNode *right{};
    
    HeadNode *down{};

}HeadNode;

子句头节点有三个成员；Num记录该行子句的数据个数，指针right指向到子句第一个数据节点，指针down指向到下一行子句。

2）子句数据节点定义：

typedef struct DataNode {
    
    int data = 0;
    
    DataNode *next{};

}DataNode;

数据节点有两个成员；data记录该数据节点的值，指针next指向下一个数据节点。

3）存储真值结构定义：

struct consequence {
    
    int value = -1;//存真值 真时为true-1，假时为false-0

};

value存入数组的某一元素的真值；若为真，value = 1；若为假，value = 0。

4）存储数独真值结构定义：

struct conse {
    
    int num = 0;
    
    int value = -1;//存真值 真时为true-1，假时为false-0

};

结构体conse有两个成员；num存储数独转换为cnf公式的数值，value存储真值；若为真，value = 1；若为假，value = 0。

5）系统总体存储结构关系

主要运用结构体HeadNode和DataNode存储数据，根据两种结构体的数据成员，下图展示出结构体之间的逻辑关系。

3. 主要算法设计

3.1 CnfParser模块

该模块主要功能是将cnf文件中的数据读取出来并将它存储到数据结构中。根据文件的特点，现做如下算法设计。算法流程如下图：

3.2 DPLLSolver模块

DPLL算法思想如下：

Status DPLL( S) {

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

while(S中存在单子句) { 

在S中选一个单子句L，并将单子句装入结果数组，value置为1；

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

if S = Φ return(TRUE);

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

}

V = S第一个数据节点数值

if DPLL（S ∪v ）return(TURE);

return DPLL(S ∪¬v);

}

1）HeadNode* IsSingleClause（HeadNode*）函数：寻找是否存在单子句。遍历头节点，若任意一行的Num存在为1的情况，即证明存在单子句，并返回单子句的指针。

2）void DeleteHeadNode(HeadNode* des, HeadNode* &src) 函数：在src指向的子句集中删掉des子句。此处应用了src的引用指针变量。

3）void DeleteDataNode(int data.HeadNode*&src) 函数：在src指向的子句集中若有节点的数值与data相等，则删除该变元所在的子句；若只是绝对值相等，则删除该变元。

4）status IsEmptyClause(HeadNode* src)函数：判断src函数中是否存在空子句，即遍历头节点，若存在头节点不为空且Num值为0的，即表示存在空子句，返回TRUE；否则，返回FALSE。

5）HeadNode* ADDSingleClause(HeadNode* src,int Var)函数：将变元Var装载成为单子句，并将该单子句装载到src的子句集中，依照函数内容，该单子句始终添加到头节点，最终返回头节点指针。

6）HeadNode* Duplication(HeadNode* src)函数：将src所指向的子句集复制一个副本，并将副本的头指针返回。

3.3 Sudoku模块

该模块功能是①创建数独终盘，②通过挖洞法创建数独初盘，○3将数独初盘转换成SAT问题并转换成cnf公式输出到文件，并返回文件名。

1）CreateSudoku模块：

伪代码如下：

void createSudoku(int a[][COL]) { //生成数独
    
    randomFirstRow(a[0],COL);//随机生成第一行
    
    Digit(a,1,0);//递归生成后i行

}

randomFirstRow函数算法流程：

Digit函数算法流程：

2）数独初盘生成模块 createStartinggrid函数算法流程：

3）数独问题转换为SAT问题

ToCnf函数模块：

以下为函数算法说明：

Billy1900/DPLL-Algorithm

About

Topics

Resources

Stars

Watchers

Forks

Releases

Packages 0

Languages

Packages