从零开始编写SAT求解器（三）

从零开始编写SAT求解器（三）

• 从零开始编写SAT求解器（三）
• • 上一篇
  • 核心算法：DPLL
  • 其他文件
  • 测试效果

从零开始编写SAT求解器（三）

上一篇

核心算法：DPLL

//DPLL.cpp
#include "DPLL.h"bool DPLL::check_sat() {// TODO: your code here, or in the header filestd::unordered_map<int,int> atomStatus;//记录节点状态0，1，2int clause_num = phi.clauses.size();//子句数量int atomNum = phi.num_variable;//变量数量for(int i=1;i<=atomNum;i++)result.insert(std::make_pair(i,true));int* nodeStatus = new int[atomNum];for(int i=0;i<atomNum;i++)nodeStatus[i]=0;int ptr = 0;//指向当前节点while(true){if(nodeStatus[ptr]==2)break;else if(nodeStatus[ptr]==0) {nodeStatus[ptr]++;result[ptr + 1] = false;}else {nodeStatus[ptr]++;result[ptr + 1] = true;}int solveStatus = 2;//0 肯定不是解，1 肯定是解，2 不确定//检查是否是解bool wholeValue = true;//整个式子的真值for(int i=0;i<clause_num;i++) //每个子句{bool currValue=false;//这个子句是不是假的bool any_notsure=false;//有没有不确定的literatureint len = phi.clauses[i].size();for(int j=0;j<len;j++){int currvar = phi.clauses[i][j];if(VAR(currvar)<=ptr+1){if((POSITIVE(currvar)&&result[currvar])||(NEGATIVE(currvar)&&!result[VAR(currvar)])){//有一个为真，子句为真currValue=true;break;}}else{any_notsure=true;}}wholeValue=wholeValue&&currValue;if(currValue||any_notsure){continue;}else{solveStatus=0;break;}}if(wholeValue)solveStatus=1;//检查完毕if(solveStatus==0)//肯定不是解，回溯{while(ptr>0&&nodeStatus[ptr]==2)ptr--;for(int i=ptr+1;i<atomNum;i++)nodeStatus[i]=0;}else if(solveStatus==1)return true;else ptr++;}return false;
}model DPLL::get_model() {// TODO: your code here, or in the header filereturn this->result;
}

其基本流程我举个例子：
假设五个变量A,B,C,D,E
我先假定A取真，其他的不确定，然后我检查输入的CNF是否为真
如果是真，那太好了，返回退出
如果不确定，那我再假定B取真，再检查
如果是假，那么回溯/取另外一个值
怎么回溯：
再举个例子：
假如ABCDE分别是1，1，1，1，null，这时发现CNF为假！
现在指针指向的是D，所以从D取另外的值，此时ABCDE分别为1，1，1，0，null
发现还是不行，CNF为假，这时就要回溯，回溯到哪？递归的搜索当前节点的父亲，直到找到这样一个节点，它还有没有取到的值（也就是说它没“脏”），或者到根节点（此时如果根节点为“脏”，证明所有情况搜索完毕，输入的CNF是不可满足的）。
回溯完成后，注意，在当前节点以下的所有节点，它们的状态都被重新标记为“干净”，也就是它们既没有取过真值，也没有取过假值，因为它们的父节点状态发生了变化，相当于它们即使与之前取同样的布尔值，ABCDE作为一个整体，这五个布尔值的组合也与之前不同。

其他文件

common.h:

#include 
#include 
#include 
#include #ifndef DPLL_COMMON_H
#define DPLL_COMMON_H// A literal is a atomic formula (that contains a variable). Like in dimacs,
// + positive numbers denote the corresponding variables;
// - negative numbers denote the negations of the corresponding variables.
// Variables are numbered from 1.
typedef int literal;
#define POSITIVE(x) ((x) > 0)
#define NEGATIVE(x) ((x) < 0)
#define VAR(x) (((x) > 0) ? (x) : (-(x)))// A clause is a list of literals (meaning their disjunction).
typedef std::vector<literal> clause;// A formula is a list of clauses (meaning their conjunction).
// We also specify the total number of variables, as some of them may not occur in any clause!
struct formula {int num_variable;std::vector<clause> clauses;formula(int n, const std::vector<clause>& clauses): num_variable(n), clauses(clauses) {}
};// A satisfying model (interpretation).
// e.g. `model[i] = false` means variable `i` is assigned to false.
typedef std::unordered_map<int, bool> model;#endif //DPLL_COMMON_H

DPLL.h:

#ifndef DPLL_DPLL_H
#define DPLL_DPLL_H#include "common.h"class DPLL {
public:DPLL(const formula &phi) : phi(phi) {}bool check_sat();model get_model();
private:formula phi;model result;
};
#endif //DPLL_DPLL_H

CMakeLists.txt:

# cmake_minimum_required(VERSION )
cmake_minimum_required(VERSION 3.15)
project(dpll)set(CMAKE_CXX_STANDARD 17)set(CMAKE_BUILD_TYPE "Debug")
set(CMAKE_CXX_FLAGS_DEBUG "$ENV{CXXFLAGS} -O0 -Wall -g -ggdb")
set(CMAKE_CXX_FLAGS_RELEASE "$ENV{CXXFLAGS} -O2 -Wall")add_executable(dpll main.cpp DimacsParser.h common.h DPLL.cpp DPLL.h common.h DPLL.h DimacsParser.h)

测试效果

输入：

c Generated with `cnfgen`
c (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>
c https://massimolauria.github.io/cnfgen
c
p cnf 12 32
1 -2 0
-1 2 0
1 3 4 0
1 -3 -4 0
-1 3 -4 0
-1 -3 4 0
3 -5 0
-3 5 0
2 6 -7 0
2 -6 7 0
-2 6 7 0
-2 -6 -7 0
4 6 8 -9 0
4 6 -8 9 0
4 -6 8 9 0
4 -6 -8 -9 0
-4 6 8 9 0
-4 6 -8 -9 0
-4 -6 8 -9 0
-4 -6 -8 9 0
5 8 -10 0
5 -8 10 0
-5 8 10 0
-5 -8 -10 0
7 11 0
-7 -11 0
9 11 -12 0
9 -11 12 0
-9 11 12 0
-9 -11 -12 0
10 -12 0
-10 12 0

输出：

本文来自互联网用户投稿，文章观点仅代表作者本人，不代表本站立场，不承担相关法律责任。如若转载，请注明出处。 如若内容造成侵权/违法违规/事实不符，请点击【内容举报】进行投诉反馈！