0x00

简介 0x01 SAT 问题简介一个 SAT 求解器是解决 SAT 问题的程序，或者一个算法实现。『SAT 问题』的全称是『布尔可满足性问题』（Boolean Satisfiability Problem）。『布尔可满足性』指的是，对于一套用布尔变量（Boolean variable）和逻辑联结词（Boolean operator）表示的逻辑表达式（下文简称『公式』（formula）），若存在至少一组对布尔变量『真』或『假』的赋值（assignment），使得这个表达式『真』，即意味着这个逻辑表达式是可满足的（satisifiable），反之则是不可满足的（unsatisfiable）。SAT 求解器的工作就是对于给定的公式，尝试得出可满足或不可满足的结论。SAT 问题是一种乍看起来很简单，但很容易令人着迷的问题（puzzle）。有一些表述起来很浅显的性质，却能极大提高求解效率。

0x01

SAT 问题的表述比如下面这个公式，要如何取$x_1...x_5$的值，从而使得这个公式为真呢？

这是一个合取范式（Conjunctive Normal Form，CNF）。在合取范式中的最小单位是如上述公式中$x_1...x_5$这样的变量，以及这些变量取反（negative，也称『取补』，complement），比如公式中出现的$\neg x_2$。这种变量或取反变量被称作『文字』（literal）。您可能注意到，上面公式中括号内的文字都是用『或』（您也可以说『并』）连接的（这种形式也被称作『析取式』，Disjunctive Form），而被括号包围起来的表达式之间则使用『与』（『交』）连接的。那么括号内的表达式被称作『子句』（clause），而完整的表达式即是『公式』了。当我们要求这个公式值为真的时候，我们也可以称作它为『命题』。

合取范式有着有趣的性质。比如上面这个命题，你并不需要尝试所有的赋值组合，而只要保证每一个子句中有一个文字值为真，那么这个公式值就为真了。比如上述例子中，我迅速扫了一眼，发现$x_1$、$\neg x_2$和$x_3$可以赋值为真，并且这几个文字之间没有互斥关系，所以就不必再看剩余的文字应如何赋值了。

关于表述 SAT 问题本身也有大量的问题值得研究，比如，基于布尔代数的运算律（结合律/交换律/包含律/分配律等），任何布尔命题都可以转化为等价的合取范式，但是这个过程是指数复杂的；再比如如何将任意的合取范式转换为每个子句中最多/严格为$k$个文字的合取范式（$k$-SAT 问题）。

一般的求解器接受的标准 SAT 表述格式被称为 DIMACS CNF。这是一个文本文件，它包含了变量数、子句数以及用整数表达的公式。比如上述公式可以表达为

c An example DIMACS CNFp cnf 5 3 1 -2  3 0-2  4 -5 0 3  4  5 0

其中以 c 开头的行是注释，辅助人类阅读，求解器会直接忽略。p 开头行是严格的用任意多空格分开的 4 个字，分别是"p"，"cnf"以及变量数和子句数。p 行以后则是公式。公式每个子句事实上是用 0 作为分割符的，换行是为了便于人类阅读。因此写成

c An example DIMACS CNFp cnf 5 31-2  3 0 -2  4 -5  0  3  4  5 0

也是合法的

0x02

求解器我本来希望通过一个周末实现一个非常简单的 CDCL SAT 求解器，但事实上我花了一个月。我首先花了一些时间去学习 SAT 问题的历史，以及一些经典算法如 DPLL。但是发现在理解这些算法的基础上，和我所能接触到的求解器（如 MiniSat，EasySAT，CaDiCaL 等）等仍然存在巨大的鸿沟。我的经验是，如果你希望了解一个机器的结构与行为的全部细节，那么最高效的途径就是做一个这样的机器出来。

事实证明也是如此，在这些相对先进的（但仍以教学与试验为主要目的）求解器中，有很多代码的写法是与编程语言的风格、对机器运行的调优，而很容易埋没算法本身的逻辑，但是这需要你先自己实现一次，厘清和算法相关的逻辑，才能识别出来一个求解器中，哪些部分属于算法框架，哪些部分是来自启发式方法的优化，哪些部分是代码的工程优化等等。如果您也在如何在代码层面落实基本的 CDCL 上遇到困难，那么希望这篇文章可以帮助到您，但是仍然殷切希望您能实现自己的求解器。

0x10

求解 SAT 所有人首先想到的用计算机求解 SAT 问题的方法就是穷举所有的变量赋值组合，来看这个合取范式的值是否为真。但很不幸，SAT 问题是第一个被确认为 NP 完全的问题，你可以将其理解为是一类无法在多项式时间内解决的问题的『标准模板』。由于 SAT 可以映射到一个多输入单输出的组合电路，所以我曾设想能不能把一个包含 48 个变量的 CNF 综合成组合电路放在 FPGA 上，然后通过 48 位的计数器穷举所有的结果。且不论这个超复杂的组合电路会产生多长的 propagation delay，假定 FPGA 工作在 500MHz，每个时钟周期都能得到结果，那么也需要

而涉及到几千个变量的问题……至少有生之年看不到了。但这便是 SAT 问题的有趣之处。尽管问题规模夸张，但是对于现代求解器，却能在毫秒级的时间找到解。

SAT 问题的求解自从 60 年代开始便被研究，同时形成了完备的算法，但是到了 90 年代 CDCL 被提出之后，SAT 求解器才变得现实，并且形成了工程框架，可以在其基础上再应用不同的优化策略。后来陆续出现了更为先进的 GRASP，zChaff，CaDiCaL，以及适于教学的 MiniSat 等。

0x11 处理 DIMACS CNF

// 重要的数据结构  let clauses  = []  let vars     = []  let propList = []
  const parse = function (text) {    let maxVar = 0;    let lits = [];        const makeVar = index => ({      index,      value: 0,      epoch: 0,      watch: {'1':[], '-1':[]}    })
    const lines = text.split(/[\n\r]+/)    for (let line of lines) {      if (line.length === 0 && line === lines.at(-1)) continue;
      switch(line[0]) {        case 'c': continue;        case 'p':          const [_, __, varsNumText, ___] = line.split(/[ \t]+/);          maxVar = parseInt(varsNumText);          vars = [...Array(maxVar + 1)]            .map((_, i) => makeVar(i))          break;        default:          let clauseLits = line            .split(/[ \t]+/)            .map(l => l.trim())            .map(l => new Lit(vars[abs(l)], sign(l)));          lits.push(...clauseLits);      }    }
    let clause = [];    for (const lit of lits)      if (lit != 0) clause.push(lit)       else addClause(clause.slice()), clause.splice(0);   } 

假定你已经将文本读入 text 中，我们先将 text 按换行符分割，处理 c 行和 p 行之后，按照变量数创建一个变量表。在这表中记载变量的赋值状态，以及 watchers 和 epoch，这两个变量属性分别在后续的传播和分析中用到。之后我们读入所有的文字（在代码实现中，『文字』（literal）通常被简称为 lit），转换为我们设计的类 Lit 的实例，并存入子句列表中。这个 Lit 类是如此实现的：

class Lit {  constructor(ref, pol) {    this.ref = ref;    this.pol = pol;  }  neg() { return new Lit(this.ref, -this.pol) }  val() { return this.ref.value * this.pol }  watch() { return this.ref.watch[this.pol]}  dropWatch(c) { this.watch().splice(this.watch().indexOf(c), 1); }  makeWatch(c) { this.watch().push(c); }
  // Mandatory for comparing with "=="  valueOf() { return this.ref.index * this.pol}}

Lit 中包含两个属性，一个是它所引用的变量 ref（因为 var 是 JS 的保留字），一个是它的正负性 pol（polarity）。值得一提的是 valueOf。在 JS 中有两种相等的比较，一种是三个等号===，它是严格地比较基本数据类型和对象的引用。如果两个分别创建的对象包含同样的属性和属性值，用===比较的结果也是假，而两个等号==的比较会首先调用左右两边对象的 valueOf 方法 。这样我们就可以简洁地比较一个文字的值是否是 1（真）、-1（假）还是 0（未定义）了。保存子句列表的方法如下：

  const assign = (lit, level, cause) => {    Object.assign(lit.ref, {value: lit.pol, level, cause});    propList.push(lit);  }
  const addClause = c => {    if (c.length === 1) {      assign(c[0], 0, [])    } else {      clauses.push(c);      c[0].neg().makeWatch(c);      c[1].neg().makeWatch(c);    }  }

至此，我们就介绍完了从读入 DIMACS 到形成求解时所需的数据结构的过程。我们得到了子句列表 clauses，变量列表 vars 以及一个还不知要干什么的 propList，但是我们知道的是，propList 中保存的都是已经被赋值的文字。可能对上述代码中所提到的 watch 还不甚了解，我们会在介绍单位子句和子句传播时详细介绍，到时您需要再回过头看这部分代码。

To be cont'd.