前言

SAT 问题简介

SAT是可满足性、适定性(Satisfiability)问题的简称。一般形式为k-适定性问题或k-可满足性问题，简称 k-SAT。

何为布尔可满足性问题？给定一条真值表达式，包含逻辑变量、逻辑与、逻辑或以及非运算符，如：
$(a\wedge \neg b\wedge (\neg (c\vee d\vee \neg a)\vee (b\wedge \neg d)))\vee (\neg (\neg (\neg b\vee a)\wedge c)\wedge d)$

是否存在一组对这些变量的赋值，使得整条式子最终的运算结果为$true$？若可以，那么这个性质被称为这条逻辑公式的可满足性（satisfiability），如何快速高效地判断任意指定逻辑公式的可满足性是理论计算机科学中的一个重要的问题，也是第一个被证明为NP-完全（NP-complete，NPC）的问题。

当$k>2$时，可满足性问题是NPC问题，因此我们一般只研究$k=2$的情况。

2-SAT算法

通常所说的2-SAT问题往往需要我们处理对于$n$个布尔变量 { x n } ( x i ∈ { 0 , 1 } ) \{x_n\}\left(x_i\in\{0,1\}\right) {xn​}(xi​∈{0,1})的$m$个限制。
其每个限制都形如一个$\vee$运算符连接的两个简单限制条件，简单限制条件为$x_i=true$（记作$x_i$）或$x_i=false$（记作$\neg x_i$），因此限制条件一共有四种：

• $s_k=x_i\vee x_j$
• $s_k=\neg x_i\vee x_j$
• $s_k=x_i\vee \neg x_j$
• $s_k=\neg x_i\vee \neg x_j$

我们需要满足：$\underset{i=1}{\stackrel{m}{\bigwedge }}{s}_i=true$
也就是需要每一个$s_k$都为真。

其处理方法为：
首先建图，对变量$x_i$建立两个点$x_{i,0},x_{i,1}$表示选$x_i=0$或$x_i=1$，然后在新图上对每个限制按照如下方式连边。
例如对于限制$s_k$，我们讨论这条限制下 a , b ∈ { 0 , 1 } a,b\in\{0,1\} a,b∈{0,1}，$x_i=a$时是否一定有$x_j=b$，如果一定有，就连有向边$x_{i,a}\to x_{j,b}$。
同理我们讨论$x_j=a$是否一定有$x_i=b$，如果一定有，就连有向边$x_{j,a}\to x_{i,b}$

感性理解这张图，如果$x_{i,a}$可达$x_{j,b}$，则说明$x_i=a$可以推出$x_j=b$，或者说$x_i=a$蕴含了$x_j=b$。

因此我们知道这个可满足性问题无解的充要条件为，存在$i$使得$x_{i,0}$和$x_{i,1}$处于同一个强连通分量内，这意味着$x_i=0$推出$x_i=1$，同时$x_i=1$推出$x_i=0$，因此无解。

因此我们可以使用Tarjan算法求强连通分量来判断2-SAT问题是否有解，事实上我们还可以输出一组可行解。
具体方法如下，首先对我们建图的图求强连通分量缩点，得到一张DAG，然后对DAG进行拓扑排序，则$x_i$对应的两个节点中，对应的强连通分量拓扑序较为靠后的节点对应的权值，是$x_i$取得的权值。
其原理是，如果$x_i=a$会推出$x_i=b$，那么就不能选$x_i=a$，此时只能选$x_i=b$。

这样我们就用Tarjan算法取得了可满足性问题的$O(n+m)$做法。

具体的连边方式

首先，所有限制都可以转化为$x_i=a\Rightarrow x_j=b$的形式进行连边，这里记录一些经典的连边方式，这样就不需要每次做转化了。

• $x_i=a\Rightarrow x_j=b$
  • $x_{i,a}\to x_{j,b}$
  • $x_{j,\neg b}\to x_{i,\neg a}$
• $a\vee b$
  • $a_0\to b_1$
  • $b_0\to a_1$
• $\neg a\vee b$
  • $a_1\to b_1$
  • $b_0\to a_0$
• $\neg a\vee \neg b$
  • $a_1\to b_0$
  • $b_1\to a_0$
• $a=true$
  • 转化为$a=0\Rightarrow a=1$
  • $a_0\to a_1$
• $a=false$
  • 转化为$a=1\Rightarrow a=0$
  • $a_1\to a_0$
• $a=b$
  • 转化为$a=1\Rightarrow b=1$，且$a=0\Rightarrow b=0$
• $a\ne b$（$a\otimes b$）
  • 转化为$a=0\Rightarrow b=1$，且$a=1\Rightarrow b=0$
• $x_1,x_2,x_3,...$至多一个为真
  • 转化为：
    • $x_1=1\Rightarrow x_2=0$，且$x_1=1\Rightarrow x_3=0$，…
    • 且$x_2=1\Rightarrow x_1=0$，且$x_2=1\Rightarrow x_3=0$，…
    • 且$x_3=1\Rightarrow x_1=0$，且$x_3=1\Rightarrow x_2=0$，…
    • …
  • 注意这样连出来的边数是$O(m^2)$级别的
• $x_1,x_2,x_3,...$至多$k>1$个为真
  • 2-sat一般不能做
• $x_1,x_2,x_3,...$至少$k\ge 1$个为真
  • 2-sat一般不能做
• $x_1,x_2,x_3,...$恰好$k\ge 1$个为真
  • 2-sat一般不能做

其中一些限制条件也可以在连边的时候判掉。

2-SAT原理

我们现在有$n$个布尔变量，称为 { x n } ( x i ∈ { 0 , 1 } ) \{x_n\}\left(x_i\in \{0,1\}\right) {xn​}(xi​∈{0,1})，现在给出$m$条限制，每一条限制都形如：
当$x_i=a$时，有$x_j=b$（ a , b ∈ { 0 , 1 } a,b\in\{0,1\} a,b∈{0,1}）
即：$x_i=a\Rightarrow x_j=b$

接下来说一下如何求解这个问题。

图的建立

点的意义

我们使用图论方法对这个问题进行求解，按照经典套路，我们需要在图上定义一个集合，然后把原问题的意义在集合内体现出来。

具体来说，我们有一个集合$S$，同时在图上有$2n$个点，其中每个比尔变量$x_i$对应两个点，一个叫做$x_{i,0}$，另一个叫做$x_{i,1}$。
我们规定$x_{i,0},x_{i,1}$当中只能恰好有一个属于集合$S$，如果$x_{i,0}\in S$，则$x_i=0$；如果$x_{i,1}\in S$，则$x_i=1$。

我们知道根据限制能够推出一些关系，例如如果$x_{i,a}\in S$，那么一定有$x_{j,b}\in S$，我们希望用边表示这一种关系，因此我们规定对于任意元素$u\in S$，$u$在图上可达的所有点$v$均属于$S$。

边的意义

刚才已经定义了图中的点，以及集合$S$。现在具体说一下图中的边是如何连接的：
对于限制：$x_i=a\Rightarrow x_j=b$

我们考虑一个一个向着集合$S$内添加元素的过程，我们必然是找到一个点$u$加入集合，然后将$u$的所有后继加入$S$，然后把这些后继的所有后继加入$S$…
由于我们知道$x_i=a$时，$x_j=b$，因此对于这个限制，我们在图上连边$x_{i,a}\to x_{j,b}$，这样就似乎可以表示这个限制了。
（注意连边方式到这里还不完全正确）

此时我们会得到一个暴力算法：

• 枚举一个未被确定的变量$x_i$
• 先选择$x_{i,0}$，然后检查$x_{i,0}$可达的所有点，我们将会选中他们。
  • 如果发生冲突（即存在$x_{j,0},x_{j,1}\in S$），那么就说明$x_i\ne 0$，回溯。
• 如果$x_{i,0}$不能选，那么就选择$x_{i,1}$，然后检查$x_{i,1}$的可达点，检查是否有冲突，如果没有就选上它们，否则就说明无解。

但是我们会发现这个算法是会错的，举例来说，对于以下两个限制：

• $y=0\Rightarrow x=1$
• $y=1\Rightarrow x=1$

我们会连出这张图：

但是如果我们一开始选择$x_0$，后来就会发现无论选择$y_0$还是$y_1$都会有矛盾，此时就输出无解，显然是不对的。

这样会出错是因为，对于这样的一条限制$y=0\Rightarrow x=1$来说，选择$x$的值是会对$y$的值产生影响的，具体来说，如果$x=0$，这就说明$y\ne 0$，即$y=1$。

换句话说，命题$y=0\Rightarrow x=1$的逆否命题$x\ne 1\Rightarrow y\ne 0$，即$x=0\Rightarrow y=1$，具有和原命题一致的真假性，因此选择$x$的值可能会对$y$造成影响，因此我们需要进一步讨论$x=a\Rightarrow y=b$说明了$x,y$之间的那些关系：

• 当我们选择了$x_a$时，必然有$y_b$
• 当我们选择了$x_{\neg a}$时，这条限制不提供任何约束，即有可能选择$y_b$或$y_{\neg b}$
• 当我们选择了$y_b$时，这条限制不提供任何约束，即有可能选择$x_a$或$x_{\neg a}$
• 当我们选择了$y_{\neg b}$时，必然有$x_{\neg a}$

因此事实上对于限制$x_i=a\Rightarrow x_j=b$来说，我们应该连接两条边：

• $x_{i,a}\to x_{j,b}$
• $x_{j,\neg b}\to x_{i,\neg a}$

此时我们再进行刚才的暴力算法，我们就获得了时间复杂度为$O(n\cdot m)$的2-sat问题的dfs做法。值得一提的是，这种做法还能同时让我们获得2-sat问题字典序最小的解。

接下来简要对暴力做法的正确性进行说明：

首先我们证明解的充分性，即我们求出的解确实是原问题的一组解：
首先我们知道，对于一个限制$x_i=a\Rightarrow x_j=b$，这个限制被违反当且仅当$x_{i,a},x_{j,\neg b}\in S$。

如果说在算法过程中$x_{i,a}$比$x_{j,\neg b}$先选的话，发生这种情况一定不可能，因为我们选择$x_{i,a}$时根据连边，一定选择了$x_{j,b}$，因此后来无法选择$x_{j,\neg b}$了，矛盾。
如果$x_{i,a}$比$x_{j,\neg b}$后选的话，这种情况还是不可能，因为根据连边的方式，如果我们选择了$x_{j,\neg b}$，我们一定选择了$x_{i,\neg a}$，不可能再选择$x_{i,a}$，因此仍然矛盾。

因此我们就证明，我们构造出的一组解满足所有限制条件，因此是一组合法解。

接下来我们证明解的必要性，即有解的时候，我们一定能够构造出一组解。
只需证明逆否命题，即如果我们构造不出一组解，此时这个问题无解。
我们考虑求解过程在决定变量$x_i$的取值时报告了无解。
此时必然是因为发生了矛盾，首先讨论选取$x_{i,0}$时候的情况，矛盾即存在元素$x_{j,0},x_{j,1}\in S$。
此时有两种情况，第一种情况是$x_{j,0},x_{j,1}$都是在$x_{i,0}$加入集合$S$后加入集合的，此时显然选择$x_{i,0}$会同时推出$x_j=0$和$x_j=1$，因此$x_i\ne 0$。

第二种情况是，$x_{j,a}$是在$x_{i,0}$加入集合$S$前加入集合的，而$x_{j,\neg a}$是因为加入$x_{i,0}$而加入集合$S$的（换句话说存在路径使得$x_{i,0}⇝x_{j,\neg a}$），这种情况不存在，这是因为，如果存在路径使得$x_{i,0}⇝x_{j,\neg a}$，由于接下来说到的性质2，我们必然知道存在一条路径使得$x_{j,a}⇝x_{i,1}$，因此当$x_{j,a}\in S$后，$x_{i,1}\in S$，这与$x_i$取值未确定矛盾，因此第二种情况不存在。

不可能存在一种情况使得$x_{j,0},x_{j,1}$在加入$x_{i,0}$前都在集合$S$内，因为这违反$S$的定义。

同理我们知道，如果在选择$x_{i,1}$的时候发生矛盾，只可能是因为$x_i\ne 1$。此时我们就得知了$x_i\ne 0$且$x_i\ne 1$，因此得到这个可满足性问题无解。

QED.

线性算法

接下来我们说一下这个问题的线性算法，线性算法是这样的：

• 对建出来的图缩强连通分量
• 这样会得到一张DAG
• 如果存在点$x_{i,0},x_{i,1}$在一个强连通分量内，则说明无解。
• 否则有解，对DAG拓扑排序，$x_i$的取值是它对应的两个点$x_{i,0},x_{i,1}$对应的强连通分量中拓扑序较靠后的那个点的取值。

证明

接下来我们证明一下线性算法的正确性。

性质1

边的对称性：
对于任意一条有向边，$(x_{i,a},x_{j,b})$，都存在有向边$(x_{j,\neg b},x_{i,\neg a})$，我们称为其对称边。

证明：
回忆建图的方式，这条性质是显然成立的。

性质2

路径的对称性：
对于任意一条从$x_{i,a}$到$x_{j,b}$的路径，必然存在对应的一条路径从$x_{j,\neg b}$到$x_{i,\neg a}$。

证明：
我们找到从$x_{i,a}$到$x_{j,b}$的路径上的每一条边的对称边，显然它们拼成一条从$x_{j\neg b}$到$x_{i,\neg a}$的路径。

算法1

我们可以据此提出一个求解2-sat问题的算法：

• 对建出来的图缩强连通分量
• 这样会得到一张DAG
• 如果存在点$x_{i,0},x_{i,1}$在一个强连通分量内，则说明无解。
• 否则有解，我们通过如下过程构造解：
  • 找到一个没有确定的$x_i$
  • 由于$x_{i,0},x_{i,1}$不强连通，因此不可能存在二者相互可达。
  • 如果有$x_{i,0}⇝x_{i,1}$，那就令$x_{i,1}\in S$。否则说明一定有$x_{i,1}⇝x_{i,0}$，或者$x_{i,0},x_{i,1}$互相不可达，此时令$x_{i,0}\in S$。
  • 如果此时我们有$x_{i,a}\in S$，那就说明有$x_{i,\neg a}\notin S$。同时说明$x_{i,a}$的所有后继都属于$S$，把它们加入$S$。
  • 同时说明$x_{i,\neg a}$的所有前驱都不属于$S$。
  • 直到所有的变量取值都确定，此时我们得到了一组可行解。

定理1

缩点后得到的DAG，满足没有任何一个$x_{i,0},x_{i,1}$强连通，是原问题有解的必要条件。

证明其逆否命题：
如果存在$x_{i,0},x_{i,1}$强连通，那么我们沿着$x_{i,0}⇝x_{i,1}⇝x_{i,0}$的回路走，上面的边对应的限制条件就说明，当$x_i=0$时$x_i=1$，并且当$x_i=1$时$x_i=0$，此时显然无解。

QED.

定理2

按照上述算法1流程构造出的解，是原问题的一组解。

证明：
如果这组解不是原问题的一组解，那么一定存在至少一个限制被违背了，设这个限制是$x_i=a\Rightarrow x_j=b$，这个限制被违反必须有$x_i=a$且$x_j=\neg b$。

假如说$x_{i,a}$比$x_{j,\neg b}$后晚加入集合，当我们加入$x_{j,\neg b}$时，由于这条限制对应连出的边，$x_{i,\neg a}$一定也会被加入集合，因此$x_{i,a}$不可能加入集合，矛盾。

否则说明$x_{i,a}$比$x_{j,\neg b}$先加入集合，但是这也不可能，因为当我们加入$x_{i,a}$时，由于这条限制对应连出的边，$x_{j,b}$也一定加入集合，因此$x_{j,b}$不可能加入集合，矛盾。

QED.

定理3

根据定理1，定理2，我们证明了：
算法1能够求出一组解，是原问题有解的充要条件。它求出的解，是原问题的一组解。

定理4

容易发现Tarjan算法+拓扑排序求解2-sat问题的过程事实上在模拟算法1，因此其的正确性也有保证。

后记

于是皆大欢喜。