许多现实生活中的问题都能通过一系列的编码转化成 SAT 问题。这里我们简单举几个例子来说明

Keller’s conjecture#

这里的“共享一个面”，指的是两个超立方体的交集恰好是它们各自的一个完整 维面，而不是只共享更低维的棱、顶点，或者面的一部分。

画成图大概是这样：

Keller 猜想是对任意维数 都成立，但实际上它在 时成立，在 时存在反例。比较反直觉的是，维数越高，超立方体可以错开的方向就越多；到了 8 维，方向多到足以让所有相邻的超立方体都只发生部分接触，而不共享完整的面。

用 SAT 证明 Keller 猜想#

Keller 猜想的证明也是 SAT 在数学里一个有名的例子，借助 Keller 图（Keller graph），我们可以把“存不存在没有共享面的铺砌”转化成有限图上的团（clique）问题。

对于给定的维数 和参数 ，我们构造图 ：

• 顶点是 里的元组；
• 如果两个顶点 在某个坐标 上满足 ，并且它们至少在两个坐标上不同，我们就让它们相邻。

这个猜想可以转化为：在图 中是否不存在一个大小为 的团？如果不存在，那么猜想成立，否则，猜想成立。

例如 画成图是这样（我们省略了边没有画出来），其共有 64 个顶点、416 条边，最大团的大小只有 2，于是 Keller 猜想在 2 维成立。

对于 来说，在加入对称性破除约束之前，编码有 39424 个变量和 200320 条子句，见 The Resolution of Keller’s Conjecture。

集合覆盖问题#

为了方便，后面把这四个集合记作 、、、。

集合覆盖本身是一个优化问题，但我们可以轻松地把它转成一个判定问题：

这个版本可以这样编码成 SAT：

我们用变量 表示集合 是否被选中， 表示选中， 表示不选。

我们要求每个元素都被覆盖，所以对全集里的每个元素 写一条子句，表示 一定在某一个子集 中：

\bigvee_{i:\, e_j \in S_i} x_i

接着，我们还要限制选中的集合数不超过 ，这可以用 基数约束 表示：

\sum x_i \leq k

基数约束可以 编码 成前文提到的 CNF 形式，于是集合覆盖问题就转成了 SAT 问题。

精确集合覆盖#

这里再看一个变形：精确集合覆盖。

还是前面那个例子，画成 0/1 矩阵会更直观：

左边选 S1、S2、S4，先不管最小化，只看“每行至少有一个 1”：e2、e4 被覆盖了两次；右边选 S1、S4，每行恰好一个 1。换句话说，精确覆盖要求每个元素只属于一个被选中的集合。

回到之前的编码方案，这就相当于在每条子句上再加一条约束：这条子句里只能有一个文字为真，也就是把子句写成：

\sum_{i:\, e_j \in S_i} x_i = 1.

我们通过大于等于&小于等于的夹逼，来得到等价的表达：

至少一个：也就是原来的子句，不用动。

\bigvee_{i:\, e_j \in S_i} x_i.

至多一个：我们用更简单的 基数约束 来表达，注意这个约束又被称为 AMO（At-Most-One），在 SAT 求解中非常常见（例如鸽笼原理）

\sum_{i:\, e_j \in S_i} x_i \leq 1.

这里注意：如果只问“存不存在精确覆盖”，那不需要额外的基数约束；如果问“存不存在不超过 个集合的精确覆盖”，才需要再补一条

\sum_i x_i \leq k.

精确覆盖的判定版本也是 NP 完全的；如果每个集合的大小都是 3，那就是经典的 X3C（Exact Cover by 3-Sets）问题。

从 SAT 的角度看，精确覆盖其实就是一个 XSAT（Exact SAT）问题：每条子句恰好有一个文字为真。XSAT 也是 NP 完全的。不过在实际求解时，专门针对精确覆盖的算法往往更好用，比如 Knuth 的 DLX（Dancing Links），以及把 DLX 和 ZDD 结合起来的 DXZ；在一些基准上，它们比直接调 SAT 求解器更高效。

精确覆盖的应用很多，比如数独、五格骨牌（pentomino）拼图等等。这个有点错误的回答 里也列了一些应用

Sudoku 数独#

在 CP 暑期学校 的时候，他们说 Sudoku 就是天生让大家理解 CSP 在做什么的例子（笑）

不过这个拿来练 SAT 编码也很合适。这里我们用 one-hot 编码：每个格子用一个长度为 9 的布尔向量，表示它填的是哪个数字。

变量#

对每个格子 和数字 ，我们引入一个布尔变量 ： 就表示格子 填 ，否则为 0。 都从 1 到 9，所以一共有 个变量。固定一个格子 ， 里恰好有一个为真，如下图所示：

约束#

每个格子恰好一个数字： 先保证至少一个：

\bigvee_{v=1}^9 x_{r,c,v}.

再保证至多一个，这里我们写成 CNF 的形式，但本质上这个就是 之前说的 AMO 约束：

\bigwedge_{1 \le v < w \le 9} (\neg x_{r,c,v} \lor \neg x_{r,c,w}).

每一行的每个数字恰好出现一次： 固定一行 和一个数字 ，我们要求这一行里恰好有一个格子填 ：

\bigvee_{c=1}^9 x_{r,c,v}
\quad\land\quad
\bigwedge_{1 \le c < c' \le 9} (\neg x_{r,c,v} \lor \neg x_{r,c',v}).

每一列的每个数字恰好出现一次：同理，固定一列 和一个数字 ：

\bigvee_{r=1}^9 x_{r,c,v}
\quad\land\quad
\bigwedge_{1 \le r < r' \le 9} (\neg x_{r,c,v} \lor \neg x_{r',c,v}).

每个 宫的每个数字恰好出现一次：固定一个宫 和一个数字 ，设 是宫里所有格子的集合：

\bigvee_{(r,c) \in B_b} x_{r,c,v}
\quad\land\quad
\bigwedge_{\substack{\{(r,c),(r',c')\} \subseteq B_b \\ (r,c) \ne (r',c')}}
(\neg x_{r,c,v} \lor \neg x_{r',c',v}).

提示：如果格子 已经给了数字 ，那就直接加一条单元子句 。

电路等价性验证#

电路等价性验证（equivalence checking）是 EDA 里很常见的一个任务，芯片设计经过综合、逻辑优化、重定时这些步骤之后，我们需要确认新电路和原电路在功能上完全一样。

但在介绍这个做法之前，我们需要先介绍一个非常重要的编码策略，通过这个策略，我们可以将任何电路编码为 SAT 问题。

Tseitin 编码#

要把 miter 交给 SAT 求解器，得先把电路转成 CNF。常用的办法是 Tseitin 变换：给每个门的输出引入一个辅助变量，然后为每个门写几条等价的子句。比如：

与门 ：

(\neg z \lor a) \land (\neg z \lor b) \land (z \lor \neg a \lor \neg b).

或门 ：

(z \lor \neg a) \land (z \lor \neg b) \land (\neg z \lor a \lor b).

异或门 ：

(a \lor b \lor \neg z) \land (a \lor \neg b \lor z) \land (\neg a \lor b \lor z) \land (\neg a \lor \neg b \lor \neg z).

Miter 电路#

假设我们有两个组合电路 和 ，它们的输入和输出都一一对应。我们可以构造一个 miter 电路：

1. 把两个电路的对应输入接在一起，让它们始终拿到同一组输入；
2. 对每一对输出 和 ，用一个异或门算出 ；
3. 把所有 用一个或门连起来，得到 miter 的输出。

M = \bigvee_{k=1}^m (y_k^1 \oplus y_k^2).

画成图是这样：

同一组输入同时喂给 C1 和 C2，对应输出 y1、y2 进异或门，再或起来得到 M。

通过这个电路，我们只需要判定：是否存在一组输入，使得 M=1？

这里本质上就是一个 SAT 问题：

• 如果答案是 UNSAT，那就说明不存在这样的输入，两个电路对所有输入都给出相同的输出，也就是等价。
• 如果答案是 SAT，那组满足赋值就是一个反例，说明两个电路在这组输入下输出不一样