复习一些数学知识#

我们首先引入一个记号 ，这是一元逻辑中所有变量的定义域

我们称 的 为布尔变量，其取值只有 0/1，也就是真/假，对于单个布尔变量，我们有一元运算如下：

其中， 为非运算。

接着，我们定义布尔变量之间的运算，其只有 两类运算，我们在下面引入记号并详细：

1. ，我们有 ，其中 表示或运算
2. ，我们有 ，其中 表示与运算

由此，我们可以定义如下布尔函数：

F(x_1, x_2, \dots, x_n): \mathbb{B}^n \rightarrow \mathbb{B}

通过上文中定义的三种运算结合构成此布尔函数，例如：

F(x_1, x_2, x_3) = (x_1 \lor x_2)\land x_3 \lor \neg(x_2 \lor x_1 \land \neg x_3)

可满足问题（SAT 问题）#

首先，我们引入一些 SAT 问题中的记号

CNF#

我们通过一些运算规则与定理，可以将任意的布尔函数都转化为合取范式的形式（ CNF），例如上式可以转为：

F^\prime(x_1, x_2, x_3) =  (x_1 \vee \neg x_2 \vee x_3)\land(\neg x_1 \lor x_3)\land(\neg x_2 \lor x_3)

也就是通过 连接的若干个 式，这里：

• 我们将 式称为 子句（clause），每个子句都是由若干个 组成
• 我们将 称为变量 对应的 文字（literal），若 ，我们将其称为正文字，若 ，我们将其称为反文字

更进一步的，在 SAT 问题中，我们还有以下名词：

• 极性（Polarity），通常指变量在子句中的出现形式，换而言之，正文字就是极性为正，反文字就是极性为负
• 赋值 （Assignments），我们可以使用此函数来表示 ，其中 ，所有变量 赋值后得到的一组有序向量，我们将其称为 CNF 的一组赋值

SAT 定义#

这样，我们可以轻松的导出 SAT 问题的定义：

值得一提的是，目前还找不到一种多项式时间的算法来解决这个问题，事实上，著名的未解问题 “P 是否等于 NP” 等价于询问这样的算法是否存在。

SAT 问题可以被认为是 “所有 NP 完全（NP-Complete）问题的起源”

我们在这里不探讨过多的计算复杂性相关的内容，如果你对这些内容感兴趣，可以阅读以下内容入门

• introduction to the theory of computation
• 怎么理解 P 问题和 NP 问题？
• 从 OIer 的角度解释什么是 P 问题、NP 问题和 NPC 问题

实例#

我们常用 .cnf 文件来描述一个 SAT 问题，例如：

p cnf 3 2
1 2 0
-1 3 0
2 -3 0

这个 .cnf 文件表示当前问题有 个变量， 条子句组成，公式的构成为：

(x_1 \lor x_2)\land(\neg x_1 \lor x_3)\land (x_2 \lor \neg x_3)

我们在后面的举例中会经常使用下面这个例子：

p cnf 7 8
-5 7 0
-1 -5 6 0
-1 -6 -7 0
-1 -2 5 0
-1 -3 5 0
-1 -4 5 0
-2 -3 -4 5 0
-1 2 3 4 5 -6 0

用图表示如下：

我们通过 的形式来说明赋值情况