从零开始编写SAT求解器（三）-白红宇

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

阅读量：4170 次

发布时间：2019-05-26

本文共 3109 字，大约阅读时间需要 10 分钟。

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

核心算法：DPLL

//DPLL.cpp#include "DPLL.h"bool DPLL::check_sat() {
       // TODO: your code here, or in the header file    std::unordered_map
   
     atomStatus;//记录节点状态0，1，2    int 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
    
     0&&nodeStatus[ptr]==2)                ptr--;            for(int i=ptr+1;i
     
      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
       
         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
        
          clauses; formula(int n, const std::vector
         
          & 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
          
            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 
   
    c https://massimolauria.github.io/cnfgencp cnf 12 321 -2 0-1 2 01 3 4 01 -3 -4 0-1 3 -4 0-1 -3 4 03 -5 0-3 5 02 6 -7 02 -6 7 0-2 6 7 0-2 -6 -7 04 6 8 -9 04 6 -8 9 04 -6 8 9 04 -6 -8 -9 0-4 6 8 9 0-4 6 -8 -9 0-4 -6 8 -9 0-4 -6 -8 9 05 8 -10 05 -8 10 0-5 8 10 0-5 -8 -10 07 11 0-7 -11 09 11 -12 09 -11 12 0-9 11 12 0-9 -11 -12 010 -12 0-10 12 0

输出：

转载地址：http://yywai.baihongyu.com/

你可能感兴趣的文章