很开心，图论的知识也是积少成多，回首往昔，我对图论的算法仅限于最短路算法($\text {dijkstra}$)和最小生成树($\text {kruskal&prime}$) 。今天来学学这个 $\text {2-SAT}$ 问题。

2-SAT简介

$\text {SAT}$ 是适定性（Satisfiability）问题的简称。一般形式为 k - 适定性问题，简称 k-SAT。而当 $k>2$ 时该问题为 NP 完全的。所以我们只研究 $k=2$ 的情况。

$\text {2-SAT}$，简单的说就是给出 个集合，每个集合有两个元素，已知若干个 ，表示 与 矛盾（其中 与 属于不同的集合）。然后从每个集合选择一个元素，判断能否一共选 个两两不矛盾的元素。显然可能有多种选择方案，一般题中只需要求出一种即可。(from OI WIKI)

我想上面说的也比我说的稍微清楚点了，那么他的现实意义是什么呢？比较常见的就是逻辑推导了。

告诉你现在有 A，B，C三个人，且A和B是男生，如果B是男生，那么C是女生。问你这三个人的性别分别是什么，我们很容易可以知道A，B为男，C为女。

现在主要就是让计算机去计算这个问题怎么办呢？首先有一点可以确定的就是，一个人不能既是男又是女。如果存在这样的断言：如果A是男，那么A是女，这样的话A只能是女，因为A不可能既是男又是女，这个规定就为我们解决 $\text {2-SAT}$ 问题提供了思路。

我们假设有 $n$ 个人，那么我们建一个 $2\times n$ 个点的有向图，第如果 $i\le n$ 那么第 $i$ 个点表示 $i$ 为男，$i>n$ 那么第 $i$ 个点表示第 $i-n$ 个人为女。$i\to j$有向边很显然表：如果选择点 $i$，那么一定要选择点 $j$，如果我们选择点 $i$ ，那么点 $i+n$ 或者是点 $i-n$ 一定不能被选中，否则我们就说点 $i$ 不能被选择。所以，如果 $i$ 与 $i$ 的对立面同时不能被选择，即它们在同一个强连通分量内，那么整个问题都是无解的，因为有一个人的性别无论怎么选始终无法满足要求。

一般情况下，解不唯一，我们通常只需要输出是否有解即可，因为如果输出方案的话它们还要设置check脚本。但是洛谷它还就搞了，神不神奇。

例题

洛谷P4782

典型的 $\text {2-SAT}$ 问题，需要注意的是，它这里每个给出的条件都是或的关系，我们需要转换成边，那么我们想想怎么转换成一条边？如果它的条件给了 $x=1 \ or\ y=1 $ 。那么 $x=1$ 和 $y=1$ 是没有什么关系的，因为 $x=1$ 的时候 $y$ 没有限制，可以为 $1$ 可以为 $0$。但是呢，如果 $x=0$ 则一定推的出 $y=1$ 因为两个必须有一个满足，一个不满足会导致另一个一定要满足。所以我们就把一个条件的反面连接到另一个条件，同样另一个条件的反面也连到这个条件。

得到了一张有向图之后呢，我们先跑 $\text {tarjan}$ 强连通分量，观察是否存在 $i\le n$ 使得 $i$ 和 $i+n$ 是否属于同一个强连通分量，如果是，则无解。如果不是，则有解。(敲黑板)，这里需要注意了啊，这里跑 $\text{tarjan}$ 需要跑 $2\times n$ 个点。如果选中 $i$ 发现产生冲突那么选择该时事件的对立面则一定不会发生冲突。这里我们跑 $\text{dfs}$ ，把与之相连的所有点都打上被选中的标记，如果存在两个状态同时被选中，则返回 $\text{false}$ 并且逐层回溯，如果到最后都没发生冲突则已选中的状态固定，继续去搜索没有被打标记的状态。直到所有的状态都有一个对应的值，最后输出这个状态。

标程

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
#include<bits/stdc++.h>
#define maxn 2000005
using namespace std;
struct eee{
    int next;
    int to;
}edge[maxn<<1],e[maxn<<1];
int root[maxn],root2[maxn],dfn[maxn],low[maxn],degree[maxn],vis[maxn],num[maxn],s[maxn],cnt,tot,top,cnt2,deep,n,m;
int sel[maxn];
void add(int x,int y){
    edge[++cnt]={root[x],y};
    root[x]=cnt;
}
void add2(int x,int y){
    e[++cnt2]={root2[x],y};
    root2[x]=cnt2;
}
void tarjan(int u){
    dfn[u]=low[u]=++deep;
    s[++top]=u;
    vis[u]=1;
    for(int i=root[u];i;i=edge[i].next){
        int v=edge[i].to;
        if(!dfn[v]){
            tarjan(v);
            low[u]=min(low[v],low[u]);
        }
        else if(vis[v]){
            low[u]=min(low[u],low[v]);
        }
    }
    if(low[u]==dfn[u]){
        vis[u]=0;
        num[u]=++tot;
        while(s[top]!=u){
            vis[s[top]]=0;
            num[s[top--]]=tot;
        }
        top--;
    }
}
int dfs(int u){
    sel[u]=1;
    if(sel[(u-1)%n+1]&&sel[(u-1)%n+n+1]){
        sel[u]=0;
        return false;
    }
    for(int i=root[u];i;i=edge[i].next){
        int v=edge[i].to;
        if(sel[v]==0){
            if(!dfs(v)){
                sel[u]=0;
                return false;
            }
        }
    }
    return true;
}
void sync(){
    ios::sync_with_stdio(0);
    cin.tie(0);
    cout.tie(0);
}
int main(){
    //freopen("1.in","r",stdin);
    sync();
    cin>>n>>m;
    while(m--){
        int x,y,z,w;
        cin>>x>>y>>z>>w;
        add(x+(y)*n,z+(!w)*n);
        add(z+(w)*n,x+(!y)*n);
    }
    for(int i=1;i<=2*n;i++){
        if(!dfn[i])tarjan(i);
    }    
    for(int i=1;i<=n;i++){
        if(num[i]==num[i+n]){
            printf("IMPOSSIBLE\n");
            return 0;
        }
    }
    for(int i=1;i<=n;i++){
        if(sel[i]==0&&sel[i+n]==0){
            if(!dfs(i)){
                dfs(i+n);
            }
        }
    }
    printf("POSSIBLE\n");
    for(int i=1;i<=n;i++){
        printf("%d ",sel[i]>sel[i+n]);
    }
    putchar(10);
    return 0;
}