2-SAT学习笔记

前置芝士

洛谷日报第157期 [HyyypRtf06]快速入手拓扑排序

洛谷日报第237期 [dzz1537568241]Tarjan，你真的了解吗？

如果想要系统学习2-SAT，请在阅读此篇文章前阅读过这两篇前置芝士的文章或者已知掌握前置芝士；如果想初步了解2-SAT是什么，也可以阅读第一部分。

本文将围绕四个部分讲述2-SAT。

1. SAT问题以及2-SAT问题的定义。

2. 2-SAT问题的朴素解法及说明。

3. 2-SAT的Tarjan解法及说明。

4. 2-SAT的例题及应用。

一、SAT问题以及2-SAT问题的定义

SAT问题就是给出 n 个 bool 变量，（变量只可能是 0 或 1 ）。m 个限制条件 。限制条件的描述可能为 a_1\ and\ a2 = 1 , a_2\ or\ a3\ xor\ a4 = 0 等，要求构造出一个合法的包含 n 个 bool 元素的序列，满足所有的限制条件，由于这个问题是一个NPC问题，无法得到时间复杂度优秀的解法，有兴趣的可以自行搜索。

退而求其次，2-SAT问题同SAT问题的条件几乎一样，唯一不同的是对于所有的限制条件只会描述 2 个 bool 变量，比如 a1\ and\ a2 = 1 , a2\ or\ a3 = 0 等。

给出一个例子，比如共有四门课：语文、数学、英语、物理。共有四位小朋友都提出了自己的两个要求，你要决定出一个合法的课程表，使其满足每个小朋友至少一个要求（当然，也可以是其他限制方法，比如说每个小朋友至少不满足一个要求，绝不仅限于此，但此处为了阅读方便选择满足每个小朋友至少一个要求）。

以上就是一个典型的2-SAT问题，课程表中只包含数学，就是一个合法的解，课程表中包含数学、物理和英语同样是一个合法的解，解不限于此。

二、2-SAT问题的朴素解法及说明

暴力解法

我们考虑枚举每一个 bool 变量是 0 还是 1 ，枚举完 n 个 bool 变量进行判断，是否满足所有 m 个限制条件，如果满足，结束枚举，如果不满足，继续枚举，下面给出两种伪代码，第一种是dfs，第二种是二进制状态枚举，最坏时间复杂度为 O(2^nm) 。

第一种写法（dfs）

bool dfs(int pos){//pos记录的是枚举到第几个bool变量
     if(pos>n){//如果枚举完n个变量就进行判断 
     if(check())return true;//返回合法
     else return false;//返回不合法
     a[pos]=true;//枚举此个变量为1
     if(dfs(pos+1))return true;//返回合法
     a[pos]=false;//枚举此个变量为0
     if(dfs(pos+1))return true;//返回合法
     return false;//返回不合法
}

第二种写法（二进制状态枚举）

bool sovle(){
     for(int i=0;i<(1<<n);i++){//枚举每一个bool元素的01情况，共有(1<<n)种情况，最大为(1<<n)-1，最小为0
         if(check(i))return true;//如果判断合法就返回合法
     }
     return false;//返回非法
}

暴力解法的优化

对于暴力解法的第二种，已经不能再优化了，但第一种dfs还是可以优化的，对于枚举完再判断可以优化为枚举每一位并进行对这一位的单独判断，关于这一位的限制条件是否合法，可以省去大量的非法状态，我们需要预处理出每一个变量各自的要求，最坏时间复杂度仍是 O(2^nm) ，伪代码如下。

bool dfs(int pos){//pos记录的是枚举到第几个bool变量
     if(pos>n)return true;//如果枚举完n个变量还没有非法就返回合法 
     a[pos]=true;//枚举此个变量为1
     if(!check(pos))return false;//不符合要求就返回非法
     if(dfs(pos+1))return true;//返回合法
     a[pos]=false;//枚举此个变量为0
     if(!check(pos))return false;//返回非法
     if(dfs(pos+1))return true;//返回合法
     return false;//返回不合法
}

三、2-SAT的Tarjan解法及说明

题目先导

给出 n 个 bool 变量， m 个限制条件，每个限制条件描述为 i\ a\ j\ b ，表示若第 i 个元素为 a ，则第 j 个元素必定为 b ，这里的 a,b 都是 bool 元素，要求构造出一个合法的序列，使其满足所有限制条件。

样例：

n=2,m=3 i=1,a=0,j=2,b=0 i=2,a=0,j=1,b=1 i=2,a=1,j=1,b=0

算法说明

动手算一下我们可以发现这个样例是由唯一解的，解的序列为： 1,0 。但如果 n,m 大一些，就无法快速得解。

若第 i 个元素为 a ，则第 j 个元素必定为 b

我们可以发现这种限制条件带有指向性，就像一条有向边，于是我们定义一条有向边 (u->v) 为若 u 成立则 v 一定成立。

但我们发现第 i 个元素可能是 0 或 1 ，无法用一个点来代表，我们可以将一个元素拆成 0 和 1 两个点，第 i 个点代表第 i 个元素为 0 的点，第 i+n 个点代表第 i 个元素为 1 的点，总共有 2n 个点，我们就获得了关于2-SAT的第一条规律。

小结：我们将一个元素拆成两个点表示 bool 元素的两种情况，有向边表示若起点成立，则终点一定成立。

比如样例里的 i=1,a=0,j=2,b=0 ，我们就可以连一条有向边 (u=1->v=2) 。

按照这种方法建好的图是下面这个样子的。

那么，为什么 1,0 是唯一的合法解呢？我们观察可以发现，如果从点 1 出发，也就是第 1 个元素为 0 ，我们必可以通过有向边推出点 2 ，也就是第 2 个元素为 0 ，继续推可以推出点 3 ，也就是第 1 个元素为 1 。

这个时候我们一旦省略掉中间点，就会发现，从点 1 一定可以推出点 3 ，也就是若第 1 个元素为 0 ，则必定第 1 个元素为 1 。但一个元素只可能是一个值，不可能同时是两个值，所以若第 1 个元素为 0 必能推出矛盾的情况，所以第 1 个元素的值不可能是 0 。

但是如果我们反过来推的话，从点 3 却不能走到点 1 ，说明若第 1 个元素的值为 1 的话，不会推导出矛盾的情况。同理，点 4 可以走到点 2 ，点 2 却不会走到点 4 ，于是第 2 个元素的值就是 0 。全序列的值就确定下来了： 1,0 ，至此我们发现了关于2-SAT的第二条规律。

读到这里，聪明的读者或许会有疑问，有的情况下建出来的图是非法的，但答案却可以推出合法？先保留这个疑问，想想有什么解决方法，在本文的后些地方会予以解答。

那么建图的代码我们就可以写出来了，伪代码如下。

int main(){
    scanf("%d%d",&n,&m);
    for(int k=1;k<=m;k++){
        scanf("%d%d%d%d",&i,&a,&j,&b);
        add(i+(n&a),j+(n&b));//如果a为0，那么i+(n&a)为i，否则为i+n，j同理
    }
    return 0;
}

小结：当拆点建图后，如果一个元素拆出的两个点 u,v 。存在有向图上的路径 (u->v) ，则点 u 可以推出点 v ，点 u 非法，则点 v 合法。

继续上面留下来的问题：如何确定一条有向图上的路径 (u->v) 呢？

为了简化问题，我们先假设我们建出来的图是一个有向无环图（DAG），那么进行拓扑排序之后，一旦存在一条 (u->v) 的路径，那么 u 的拓扑序一定小于 v 的拓扑序，也就是说一个元素拆点后合法的点的拓扑序一定大于非法点。

将上文的例子进行添加后如下图。

红色箭头所表示是拓扑序的遍历顺序为 4->1->2->3 。

还记得我们的合法序列吗？序列为 1,0 ，合法点为点 2 和点 3 ，合法点点 2 对应的非法点是点 4 ，合法点点 3 对应的非法点是点 2 ，我们发现一个元素的合法点拓扑序确实比非法点的拓扑序大，至此我们获得了2-SAT的第三条规律。

小结：有向无环图的情况下，合法点的拓扑序比非法点大。

我们有了有向无环图下的优秀做法，时间复杂度 O(n+m) 伪代码如下。

void topo(){//拓扑
     int tot=0;//拓扑序计数
     queue<int>q;//队列
     for(int i=1;i<=2*n;i++){
         if(!in[i])q.push(i),ord[i]=++tot;//如果入度为0就入队
     }
     while(!q.empty()){
         int u=q.front();//取队头
         q.pop();//弹出队头
         for(int i=head[x];i;i=e[i].nex){//链式前向星
             int v=e[i].to;
             in[v]--;//v的入度减1
             if(!in[v]){//如果入度为0
                 q.push(v);//入队
                 tot++;//拓扑序+1
                 ord[v]=tot;//记录拓扑序
             }
         }
     }
     for(int i=1;i<=n;i++){
         if(ord[i]>ord[i+n])printf("0 ");//如果点i的拓扑序大于点i+n，选点i，为0
         else printf("1 ");//否则选点i+n，为1
     }
     printf("\n");
}

但是我们建的图不保证无环，只保证是一个有向图，那什么算法可以将一个有向图变成有向无环图呢？就是Tarjan的强联通算法了，本文的前置芝士包含了这一内容。

Tarjan的强联通算法可以在 O(n+m) 的时间内求出一个有向图的所有强连通分量，这样有向图就变成了有向无环图。

强连通分量的性质：一个强连通分量里的任意两个点可以互相到达，意思就是只要任意强连通分量里的任意一个点合法，强连通分量的其它所有点都合法，任意两个点之间都有以一条以对方为起点自己为终点和自己为起点对方为终点的路径。

那么如何判断这种情况下的拓扑序大小呢？请看如下的这张图。

根据我们前面的几个小结可以推出点 1 和点 4 是合法点，因为点 4 的拓扑序比点 2 大，点 1 的拓扑序比点 3 大。

但我们并不需要在执行完Tarjan算法后缩点拓扑，只需要判断一个元素的两个点的强连通分量编号哪个小就行，小的就是合法的，为什么呢？可以自己照着上面的图试着推一下，再想一下原因。

如果暂时想不出来没关系，再看下面这张图。

这就是执行完Tarjan强连通分量算法之后的图，红色字体所代表的就是这个点强连通分量编号，绿色字体所代表的是缩点之后的拓扑序。一共有 3 个强联通分量，考虑到遍历顺序的不同，所以有的点会有 2/3 ，合法点的强连通分量编号始终比对应的非法点的分量编号要小，这是为什么呢？

可以有这这种方式理解：如果跑完Tarjan缩点之后呈现出的拓扑序更大，在Tarjan会更晚被遍历到，就会更早地被弹出栈而缩点，分量编号会更小。

或者，如果一个元素拆出的两个点 u,v ，存在 (u->v) 的路径，而不存在 (v->u) 的路径，那么遍历到 v 时不会遍历到 u ，但遍历到 u 的时候一定会继续遍历到 v ，这样一定可以保证 v 更早被弹出栈和缩点，其强连通分量编号一定更小， v 就是合法点，至此我们获得了2-SAT的第四条规律。

小结：Tarjan后同一元素拆点强连通分量编号小的点是合法点。

读到这里不知道你有没有发现，我们只考虑了一个元素的拆出的两个点中只有一个点可以到达另一个点的情况，如果两个点可以彼此到达呢？那又该怎么办呢？

其实很好想，如果两个点可以彼此到达，说明两个点Tarjan后肯定在同一个强连通分量里，但如果看到前面加粗的字体：强连通分量的性质，就会知道，只要强连通分量里有一点合法，其它点都会合法，两个点彼此到达，说明两个点彼此合法。但一个元素拆成的两个点只会有一个点合法，所以是矛盾的，是非法的，一个元素没有合法解，整个序列就没有合法解。至此我们得到了2-SAT的第五条规律。

小结：如果一个元素拆成的两个点在同一个强连通分量里，即强连通分量编号相同，那么整个序列无解。

那么，如果拆点后的两个点之间无法从某一点到达另一点，也就是两点间没有相连的路径，该怎么办呢？

其实也很好想，两点间无相连的路径，也就是说从任意一点出发无法到达对应的另一点，也就是推不出矛盾状态，也就是两点都可以是合法状态，随意选一点合法即可，那么归到上面判断强联通分量编号小的合法讨论里取点即可，因为这两点间都没有一条有向路径，更不可能强联通，编号自然不一样，至此我们得到了2-SAT的第六条规律。

小结：如果一个元素拆成的两个点之间没有任何路径相连，即使是有向路径，那么这两点都可以成为合法点，这两点的分量编号不同，选小的即可。

伪代码如下。

struct node{
    int to,nex;
}e[maxm];
int dfncnt,sccnum,scc[maxn],dfn[maxn],low[maxn],s[maxn],top;
void add(int u,int v){//链式前向星
    e[++cnt].to=v,e[cnt].nex=head[u],head[u]=cnt;
}
void tarjan(int u){//tarjan求强联通
    dfn[u]=low[u]=++dfncnt;
    s[++top]=u;
    for(int i=head[u];i;i=e[i].nex){
        int v=e[i].to;
        if(!dfn[v]){
            tarjan(v);
            low[u]=Min(low[u],low[v]);
        }
        else if(!scc[v]){
            low[u]=Min(low[u],low[v]);
        }
    }
    if(dfn[u]==low[u]){//弹栈
        ++sccnum;
        while(s[top]!=u){
            scc[s[top]]=sccnum;//强连通分量编号
            top--;
        }
        scc[s[top]]=sccnum;
        top--;
    }
}
int main(){
    scanf("%d%d",&n,&m);
    for(int k=1;k<=m;k++){
        int i,a,j,b;
        scanf("%d%d%d%d",&i,&a,&j,&b);
        add(i+(n&a),j+(n&b));
    }
    for(int i=1;i<=2*n;i++){//一共2n个点
        if(!dfn[i])tarjan(i);
    }
    for(int i=1;i<=n;i++){
        if(scc[i]==scc[i+n]){//编号相同非法
            printf("IMPOSSIBLE");
            return 0;
        }
    }
    for(int i=1;i<=n;++i){
        if(scc[i]<scc[i+n])printf("0 ");//编号小的合法
        else printf("1 ");
    }
    return 0;
}

总结：

1. 我们将一个元素拆成两个点表示 bool 元素的两种情况，有向边表示若起点成立，则终点一定成立。

2. 当拆点建图后，如果一个元素拆出的两个点 u,v 。存在有向图上的路径 (u->v) ，则点 u 可以推出点 v ，点 u 非法，则点 v 合法。

3. 有向无环图的情况下，合法点的拓扑序比非法点大。

4. Tarjan后同一元素拆点强连通分量编号小的点是合法点。

5. 如果一个元素拆成的两个点在同一个强连通分量里，即强连通分量编号相同，那么整个序列无解。

6. 如果一个元素拆成的两个点之间没有任何路径相连，即使是有向路径，那么这两点都可以成为合法点，这两点的分量编号不同，选小的即可。

四、2-SAT的例题及应用

2-SAT的原理如出一辙，关键是建边的关系，所以接下来的例题只会给出建图方法。

建边方式提醒：第三部分的例题，细心的读者可以发现，我们将 (u->v) 描述为若 u 成立则 v 成立，表示肯定的推导关系，但还有一种肯定的推导关系，即若 v 不成立则 u 一定不成立，定义 v',u' 为 v,u 拆点后的对应点。即再连边 (v'->u') 这样所有的肯定的推导关系使用后才能获得合法解。

所以，建2-SAT图，必须将所有肯定关系都找出建边，否则可能会出纰漏，这里回答的是本文上面的读者思考部分。

建边方式如图。

建边小练习：

（1） 2-SAT问题，要求对于每个限制条件的两个 bool 元素的要求至少不满足 1 个，求建边方法。

解：至少不满足一个说明若一个元素合法，则另一个元素一定不合法，连边 (u->v'),(v->u') 。

（2） 2-SAT问题，要求对于每个限制条件的两个 bool 元素的要求至少满足 1 个，求建边方法。

解：至少满足说明若一个元素不合法，则另一个元素一定合法，连边 (u'->v),(v'->u) 。

（3） 2-SAT问题，每个限制条件的两个元素要求若第一个要求非法，则第二个要求一定非法，求建边方法。

解：同上面开始时的建边方式讲解大体一样，除题目要求的条件外还有隐含的若第二个要求合法，则第一个要求一定合法的条件，连边 (u'->v'),(v->u) 。

（4）2-SAT问题，要求对于每个条件给出的两个元素的值 a\ xor\ b=0 ，求元素 u,v 建边方法。

解：当 a=1,b=1 或 a=0,b=0 时条件成立，所以只要一个元素确定，另一个元素与之相同，连 (u->v)(v->u)(u'->v')(v'->u') 。

1. 第一个例题：【模板】2-SAT问题。题目要求每个限制条件至少满足一个 bool 变量的要求，即若一个变量不合要求，同一条件的另一个变量必须符合要求，连两条边即可。
2. 第二个例题：[JSOI2010]满汉全席。问题简化后建边方式同第二个例题一样，不再多叙。
3. 第三个例题：[NOI2017]游戏。将3-SAT转换为2-SAT，枚举每一个 x 赛场是 a 还是 b ，将其变成普通赛场，建边方式为若 i 为 a ，则 j 为 b ，若 j 不为 b ，则 i 不为 a ，于是连两条边，对于所有状态有合法即退出，非法即继续枚举tarjan，最坏时间复杂度 O(2^d(n+m)) 。

完结撒花！