从零开始编写SAT求解器

Tattoo

发布日期: 2020-06-27 16:35:56 浏览量: 64
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接https://blog.csdn.net/swy_swy_swy/article/details/104889142
原文链接https://blog.csdn.net/swy_swy_swy/article/details/104979621
原文链接https://blog.csdn.net/swy_swy_swy/article/details/105019684

一、源起

最近在github上看到了非常有名的cryptominisat开源项目。目前的SAT问题自动求解器有在线版的MiniSAT,但是这个需要科学上网。正好最近一直在写Java和python,C++有点生疏,而网上有大神用Haskell实现了简易的SAT求解器,就想用C++写一个自己的SAT求解器。(C++是最棒的语言)

二、背景知识

2.1 SAT问题

SAT问题是布尔可满足性问题(又名命题可满足性问题)的缩写,即给定一个布尔公式,判断是否存在满足它的解释的问题。SAT问题是第一个被证明的NP问题。这里,我把问题简化为:输入一个析取范式(CNF),输出一个布尔值表示它是否是可满足的,若它是可满足的,再输出一个使它为真的解释。

2.2 DIMACS文件

DIMACS文件是对于CNF形式的命题公式的一种简单的ASCII表示,它的结构为:

  • 开头是几行注释,以字符 ’c’ 开头

  • 注释行之后,是一个文件头,格式为 p cnf nvars nclauses,这里nvars是公式中变量的数量,nclauses是命题中子句的数量

  • 在文件头之后,每一行代表一个子句。一个子句是一系列空格分隔的非零整数,最后以0结尾。一个正数代表对应的变量(从1到nvars),一个负数代表对应变量的非

举个例子

  1. c A simple example
  2. p cnf 3 3
  3. -1 2 0
  4. -2 3 0
  5. -1 -3 0

它代表的公式是:

2.3 DPLL算法

DPLL算法是一个判断命题公式可满足性的算法,本质上是一个深度优先搜索算法。基本思想为:首先假定一个变量的值(真/假),然后检查当前条件下命题公式是否为真,若为真,程序退出,返回可满足以及一个使命题公式为真的解释;若为假,则回溯(可能改变当前变量的假定值,或退到之前的某个变量);若为假且没有变量可以回溯,程序退出,返回该公式是不可满足的。

三、项目架构

main函数如下:

  1. #include <chrono>
  2. #include "common.h"
  3. #include "DimacsParser.h"
  4. #include "DPLL.h"
  5. int main(int argc, char **argv) {
  6. //argc=2;
  7. if (argc < 2) {
  8. std::cerr << "error: no input files" << std::endl;
  9. return 1;
  10. }
  11. for (int i = 1; i < argc; i++) {
  12. std::string f(argv[i]);
  13. //std::string f="tests\\test5.dimacs";
  14. std::cout << f << std::endl;
  15. formula phi = DimacsParser::parse(f);
  16. // timer start
  17. auto start = std::chrono::steady_clock::now();
  18. DPLL solver(phi);
  19. bool sat = solver.check_sat();
  20. model m;
  21. if (sat) {
  22. m = solver.get_model();
  23. }
  24. auto end = std::chrono::steady_clock::now();
  25. // timer end
  26. if (sat) {
  27. std::cout << " sat" << std::endl;
  28. for (const auto &p : m) {
  29. std::cout << " " << p.first << " -> " << p.second << std::endl;
  30. }
  31. } else {
  32. std::cout << " unsat" << std::endl;
  33. }
  34. auto duration = std::chrono::duration_cast<std::chrono::duration<double>>(end - start);
  35. std::cout << " time: " << duration.count() << std::endl;
  36. }
  37. return 0;
  38. }

采用命令行输入,首先判断参数合法性,若合法,读入文件,将文件解析,返回自定义的formula对象。接着调用DPLL方法,返回是否可解;若可解,输出一个可行的解。可行解使用map存储。

那么,接下来的任务就是实现文件解析、DPLL核心算法。

四、文件解析器

  1. //
  2. // Dimacs parser.
  3. //filename:DimacsParser.h
  4. //
  5. #include <iostream>
  6. #include <fstream>
  7. #include <cstdlib>
  8. #include <cassert>
  9. #include "common.h"
  10. #ifndef DPLL_DIMACSPARSER_H
  11. #define DPLL_DIMACSPARSER_H
  12. class DimacsParser {
  13. public:
  14. /**
  15. * Parse a dimacs file.
  16. * @param file_name dimacs file name
  17. * @return a parsed formula (if succeeds)
  18. */
  19. static formula parse(const std::string &file_name) {
  20. std::ifstream fin(file_name);
  21. if (!fin) {
  22. std::cerr << "file not found: " << file_name << "'" << std::endl;
  23. std::exit(1);
  24. }
  25. int n = 0, m = 0;
  26. while (!fin.eof()) {
  27. char ch;
  28. fin >> ch;
  29. if (ch == 'c') { // c-line: comment
  30. char buf[1024];
  31. fin.getline(buf, 1024);
  32. } else if (ch == 'p') { // p-line: clauses will begin
  33. std::string buf;
  34. fin >> buf;
  35. assert(buf == "cnf");
  36. fin >> n >> m;
  37. break;
  38. } else { // unexpected line
  39. std::cerr << "parse error at char '" << ch << "'" << std::endl;
  40. std::exit(1);
  41. }
  42. }
  43. // clauses begin
  44. std::vector<clause> clauses;
  45. for (int i = 0; i < m; i++) {
  46. clause c;
  47. while (!fin.eof()) {
  48. int v;
  49. fin >> v;
  50. if (v == 0) {
  51. clauses.push_back(c);
  52. break;
  53. }
  54. assert(VAR(v) <= n);
  55. c.push_back(v);
  56. }
  57. }
  58. assert(clauses.size() == m);
  59. return formula(n, clauses);
  60. }
  61. };
  62. #endif //DPLL_DIMACSPARSER_H

五、assert宏

assert宏的原型定义在<assert.h>中,其作用是如果它的条件返回错误,则终止程序执行,原型定义:

  1. #include <assert.h>
  2. void assert( int expression );

assert的作用是现计算表达式 expression ,如果其值为假(即为0),那么它先向stderr打印一条出错信息,然后通过调用 abort 来终止程序运行。

请看下面的程序清单badptr.c:

  1. #include <stdio.h>
  2. #include <assert.h>
  3. #include <stdlib.h>
  4. int main( void )
  5. {
  6. FILE *fp;
  7. fp = fopen( "test.txt", "w" );//以可写的方式打开一个文件,如果不存在就创建一个同名文件
  8. assert( fp ); //所以这里不会出错
  9. fclose( fp );
  10. fp = fopen( "noexitfile.txt", "r" );//以只读的方式打开一个文件,如果不存在就打开文件失败
  11. assert( fp ); //所以这里出错
  12. fclose( fp ); //程序永远都执行不到这里来
  13. return 0;
  14. }

执行这个文件,输出:

  1. [root@localhost error_process]# gcc badptr.c
  2. [root@localhost error_process]# ./a.out
  3. a.out: badptr.c:14: main: Assertion `fp'' failed.

使用assert的缺点是,频繁的调用会极大的影响程序的性能,增加额外的开销。

在调试结束后,可以通过在包含#include <assert.h>的语句之前插入 #define NDEBUG 来禁用assert调用,示例代码如下:

  1. #include <stdio.h>
  2. #define NDEBUG
  3. #include <assert.h>

用法总结与注意事项

  • 在函数开始处检验传入参数的合法性,如:

    1. int resetBufferSize(int nNewSize)
    2. {
    3. //功能:改变缓冲区大小,
    4. //参数:nNewSize 缓冲区新长度
    5. //返回值:缓冲区当前长度
    6. //说明:保持原信息内容不变 nNewSize<=0表示清除缓冲区
    7. assert(nNewSize >= 0);
    8. assert(nNewSize <= MAX_BUFFER_SIZE);
    9. ...
    10. }
  • 每个assert只检验一个条件,因为同时检验多个条件时,如果断言失败,无法直观的判断是哪个条件失败
    “不好”例子:

    1. assert(nOffset>=0 && nOffset+nSize<=m_nInfomationSize);

    “好”例子:

    1. assert(nOffset >= 0);
    2. assert(nOffset+nSize <= m_nInfomationSize);
  • 不能使用改变环境的语句,因为assert只在DEBUG个生效,如果这么做,会使用程序在真正运行时遇到问题
    “错误”例子:

    1. assert(i++ < 100)

    “正确”例子:

    1. assert(i < 100)
    2. i++;
  • assert和后面的语句应空一行,以形成逻辑和视觉上的一致感

  • 有的地方,assert不能代替条件过滤

六、核心算法 DPLL

  1. //DPLL.cpp
  2. #include "DPLL.h"
  3. bool DPLL::check_sat() {
  4. // TODO: your code here, or in the header file
  5. std::unordered_map<int,int> atomStatus;//记录节点状态0,1,2
  6. int clause_num = phi.clauses.size();//子句数量
  7. int atomNum = phi.num_variable;//变量数量
  8. for(int i=1;i<=atomNum;i++)
  9. result.insert(std::make_pair(i,true));
  10. int* nodeStatus = new int[atomNum];
  11. for(int i=0;i<atomNum;i++)
  12. nodeStatus[i]=0;
  13. int ptr = 0;//指向当前节点
  14. while(true){
  15. if(nodeStatus[ptr]==2)
  16. break;
  17. else if(nodeStatus[ptr]==0) {
  18. nodeStatus[ptr]++;
  19. result[ptr + 1] = false;
  20. }
  21. else {
  22. nodeStatus[ptr]++;
  23. result[ptr + 1] = true;
  24. }
  25. int solveStatus = 2;//0 肯定不是解,1 肯定是解,2 不确定
  26. //检查是否是解
  27. bool wholeValue = true;//整个式子的真值
  28. for(int i=0;i<clause_num;i++) //每个子句
  29. {
  30. bool currValue=false;//这个子句是不是假的
  31. bool any_notsure=false;//有没有不确定的literature
  32. int len = phi.clauses[i].size();
  33. for(int j=0;j<len;j++)
  34. {
  35. int currvar = phi.clauses[i][j];
  36. if(VAR(currvar)<=ptr+1)
  37. {
  38. if((POSITIVE(currvar)&&result[currvar])||(NEGATIVE(currvar)&&!result[VAR(currvar)])){//有一个为真,子句为真
  39. currValue=true;
  40. break;
  41. }
  42. }
  43. else{
  44. any_notsure=true;
  45. }
  46. }
  47. wholeValue=wholeValue&&currValue;
  48. if(currValue||any_notsure){
  49. continue;
  50. }
  51. else{
  52. solveStatus=0;
  53. break;
  54. }
  55. }
  56. if(wholeValue)
  57. solveStatus=1;
  58. //检查完毕
  59. if(solveStatus==0)//肯定不是解,回溯
  60. {
  61. while(ptr>0&&nodeStatus[ptr]==2)
  62. ptr--;
  63. for(int i=ptr+1;i<atomNum;i++)
  64. nodeStatus[i]=0;
  65. }
  66. else if(solveStatus==1)
  67. return true;
  68. else ptr++;
  69. }
  70. return false;
  71. }
  72. model DPLL::get_model() {
  73. // TODO: your code here, or in the header file
  74. return this->result;
  75. }

其基本流程我举个例子:

  • 假设五个变量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

  1. #include <vector>
  2. #include <unordered_map>
  3. #include <string>
  4. #include <sstream>
  5. #ifndef DPLL_COMMON_H
  6. #define DPLL_COMMON_H
  7. // A literal is a atomic formula (that contains a variable). Like in dimacs,
  8. // + positive numbers denote the corresponding variables;
  9. // - negative numbers denote the negations of the corresponding variables.
  10. // Variables are numbered from 1.
  11. typedef int literal;
  12. #define POSITIVE(x) ((x) > 0)
  13. #define NEGATIVE(x) ((x) < 0)
  14. #define VAR(x) (((x) > 0) ? (x) : (-(x)))
  15. // A clause is a list of literals (meaning their disjunction).
  16. typedef std::vector<literal> clause;
  17. // A formula is a list of clauses (meaning their conjunction).
  18. // We also specify the total number of variables, as some of them may not occur in any clause!
  19. struct formula {
  20. int num_variable;
  21. std::vector<clause> clauses;
  22. formula(int n, const std::vector<clause>& clauses): num_variable(n), clauses(clauses) {}
  23. };
  24. // A satisfying model (interpretation).
  25. // e.g. `model[i] = false` means variable `i` is assigned to false.
  26. typedef std::unordered_map<int, bool> model;
  27. #endif //DPLL_COMMON_H

DPLL.h

  1. #ifndef DPLL_DPLL_H
  2. #define DPLL_DPLL_H
  3. #include "common.h"
  4. class DPLL {
  5. public:
  6. DPLL(const formula &phi) : phi(phi) {}
  7. bool check_sat();
  8. model get_model();
  9. private:
  10. formula phi;
  11. model result;
  12. };
  13. #endif //DPLL_DPLL_H

CMakeLists.txt

  1. # cmake_minimum_required(VERSION <specify CMake version here>)
  2. cmake_minimum_required(VERSION 3.15)
  3. project(dpll)
  4. set(CMAKE_CXX_STANDARD 17)
  5. set(CMAKE_BUILD_TYPE "Debug")
  6. set(CMAKE_CXX_FLAGS_DEBUG "$ENV{CXXFLAGS} -O0 -Wall -g -ggdb")
  7. set(CMAKE_CXX_FLAGS_RELEASE "$ENV{CXXFLAGS} -O2 -Wall")
  8. add_executable(dpll main.cpp DimacsParser.h common.h DPLL.cpp DPLL.h common.h DPLL.h DimacsParser.h)

八、测试效果

8.1 输入

  1. c Generated with `cnfgen`
  2. c (C) 2012-2016 Massimo Lauria <lauria.massimo@gmail.com>
  3. c https://massimolauria.github.io/cnfgen
  4. c
  5. p cnf 12 32
  6. 1 -2 0
  7. -1 2 0
  8. 1 3 4 0
  9. 1 -3 -4 0
  10. -1 3 -4 0
  11. -1 -3 4 0
  12. 3 -5 0
  13. -3 5 0
  14. 2 6 -7 0
  15. 2 -6 7 0
  16. -2 6 7 0
  17. -2 -6 -7 0
  18. 4 6 8 -9 0
  19. 4 6 -8 9 0
  20. 4 -6 8 9 0
  21. 4 -6 -8 -9 0
  22. -4 6 8 9 0
  23. -4 6 -8 -9 0
  24. -4 -6 8 -9 0
  25. -4 -6 -8 9 0
  26. 5 8 -10 0
  27. 5 -8 10 0
  28. -5 8 10 0
  29. -5 -8 -10 0
  30. 7 11 0
  31. -7 -11 0
  32. 9 11 -12 0
  33. 9 -11 12 0
  34. -9 11 12 0
  35. -9 -11 -12 0
  36. 10 -12 0
  37. -10 12 0

8.2 输出

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

79
文章数
34
评论数
eject