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

源起

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

背景知识

SAT问题

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

DIMACS文件

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

开头是几行注释，以字符’c’开头
注释行之后，是一个文件头，格式为p cnf nvars nclauses，这里nvars是公式中变量的数量，nclauses是命题中子句的数量
在文件头之后，每一行代表一个子句。一个子句是一系列空格分隔的非零整数，最后以0结尾。一个正数代表对应的变量（从1到nvars），一个负数代表对应变量的非。

举个例子：

 c A simple examplep cnf 3 3-1 2 0-2 3 0-1 -3 0

它代表的公式是
(¬P1∨P2)∧(¬P2∨P3)∧(¬P1∨¬P3)(\neg{P_1}\vee{P_2})\wedge(\neg{P_2}\vee{P_3})\wedge(\neg{P_1}\vee{\neg{P_3}})(¬P1∨P2)∧(¬P2∨P3)∧(¬P1∨¬P3)

DPLL算法

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

项目架构

main函数如下：

#include <chrono>#include "common.h"
#include "DimacsParser.h"
#include "DPLL.h"int main(int argc, char **argv) {//argc=2;if (argc < 2) {std::cerr << "error: no input files" << std::endl;return 1;}for (int i = 1; i < argc; i++) {std::string f(argv[i]);//std::string f="tests\\test5.dimacs";std::cout << f << std::endl;formula phi = DimacsParser::parse(f);// timer startauto start = std::chrono::steady_clock::now();DPLL solver(phi);bool sat = solver.check_sat();model m;if (sat) {m = solver.get_model();}auto end = std::chrono::steady_clock::now();// timer endif (sat) {std::cout << "  sat" << std::endl;for (const auto &p : m) {std::cout << "    " << p.first << " -> " << p.second << std::endl;}} else {std::cout << "  unsat" << std::endl;}auto duration = std::chrono::duration_cast<std::chrono::duration<double>>(end - start);std::cout << "  time: " << duration.count() << std::endl;}return 0;
}

采用命令行输入，首先判断参数合法性，若合法，读入文件，将文件解析，返回自定义的formula对象。接着调用DPLL方法，返回是否可解；若可解，输出一个可行的解。可行解使用map存储。
那么，接下来的任务就是实现文件解析、DPLL核心算法。