文章总览：高大的背影

2-SAT 一开始觉得听玄学的，学了之后有感觉没什么好写，这篇文章简单说一下罢。

  1. SAT 问题的定义
  2. SAT 问题的解法
  3. SAT 问题的例题
  4. SAT 问题的细节

经典模型：紧紧的拥抱

  • SAT 问题的定义

首先我们了解一下 SAT 问题的定义。SAT 是英文单词适定性（Satisfiability）的简称，一般来说对于 k - 适定性问题，我们都简称为 k-SAT，这篇文章要讲的就是 2-SAT 问题，这是因为当 $k>2$ 的时候 k-SAT 问题是 NPC 问题（但是好像也有解决 k-SAT 的算法）总而言之，这里研究的是 2-SAT 问题。

简单的概括最基础的 2-SAT 的核心，就是对于 $n$ 个二元组。且存在一些形如 $\langle a,b\rangle$ 的矛盾关系，这代表 $a,b$ 不能被同时选中，这里保证 $a,b$ 不属于同一个二元组。问题就是要问存不存在一种方案，使得每一个二元组都选择出一个元素并且不出现矛盾的情况，有时还会让你输出具体的方案，显然方案是不唯一的。

其实这个问题其实并不难看出是可以抽象为图论的，有人的第一直觉就是二分图，但事实上不是，但是也算是比较接近了罢，接下来我们来看如何解决这类 2-SAT 问题。

算法简介：冰冷的钢甲

  • SAT 问题的解法

首先我们可以注意到，在对于一些矛盾情况，我们会做出必然的选择。由于每个二元组都需要选出一个点，如果这两个二元组中的元素 $a_1,a_2,b_1,b_2$ 中满足了 $a_1,b_1$ 矛盾。那么对于这两个二元组中，如果我选择了 $a_1$ 那么只能选 $b_2$，如果选择了 $b_1$ 我们只能选 $a_2$，这就是必须得选的情况。那么根据这类必须得选的关系，我们可以建立起一个图。

但这个图显然不是二分图，或者 DAG，或者什么其他特殊的图，这只是单纯的一个有向图。题目让我们求的非法情况显然只有两种：

  1. 出现矛盾
  2. 一个二元组选出了两个数

如果我们按照这个逻辑建图的话，可以规避所有矛盾的情况，但是无法避免一个二元组选出了两个数。这时候，我们就应该快速判断什么时候一个二元组会出现两个数。学过小学数学的都知道，我们贪心的考虑，在有选择的时候绝对不会触犯上面的两条规则，所以说当我们固定了第一条，第二条的违反是无法选择的，也就是说只要出现了第二条，那么就是非法情况了。

由于我们的边是必然的选择，我们顺着这些边，发现了同时选中二元组两个数的内容，那么就算是违法了。而这种能够同时选中二元组两个数的情况，一定在同一个强连通分量里面，因为他们能互相推导，那么其实就是一个环（或类似于环）那么就是同一个强连通分量内了。

常见例题：家人的温暖

  • SAT 问题的例题

那么就以上面最经典的模型来说，可以写出下面的代码：

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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
#include<cstdio>
#include<iostream>
#include<algorithm>
#include<queue>
#include<map>
#include<vector>
#include<set>
#include<string>
#include<cmath>
#include<cstring>
#include<stack>
using namespace std;

typedef long long ll;
// typedef __int128 int128;
typedef pair<int , int > pii;
typedef unsigned long long ull;

namespace FastIO 
{
    // char buf[1 << 20], *p1, *p2;
    // #define getchar() (p1 == p2 && (p2 = (p1 = buf) + fread(buf, 1, 1 << 20, stdin), p1 == p2) ? EOF : *p1++)
    template<typename T> inline T read(T& x) {
        x = 0;
        int f = 1;
        char ch;
        while (!isdigit(ch = getchar())) if (ch == '-') f = -1;
        while (isdigit(ch)) x = (x << 1) + (x << 3) + (ch ^ 48), ch = getchar();
        x *= f;
        return x;
    }
    template<typename T, typename... Args> inline void read(T& x, Args &...x_) {
        read(x);
        read(x_...);
        return;
    }
    inline ll read() {
        ll x;
        read(x);
        return x;
    }
};
using namespace FastIO;

template<int N, int M>
class Graph {
    private :
        struct Edge {
            int to, nt;
            ll wt, fl;
            Edge() {}
            Edge(int to, int nt, ll wt, ll fl) : to(to), nt(nt), wt(wt), fl(fl) {}
        }e[M];
        int hd[N], cnte;
    public :
        inline void clear() { memset(hd, 0, sizeof(hd)), cnte = 0; }
        inline void AddEdge(int u, int v, ll w = 0, ll f = 0) {
            e[++cnte] = Edge(v, hd[u], w, f);
            hd[u] = cnte;
        }
        inline int head(int u) { return hd[u]; }
        inline int nt(int u) { return e[u].nt; }
        inline int to(int u) { return e[u].to; }
        inline ll wt(int u) { return e[u].wt; }
        inline ll& fl(int u) { return e[u].fl; }
};

const int N = 1010;

int n, m;
Graph< N << 1, N * N >G;

inline void Input() {
    // if(scanf("%d%d", &n, &m) != 2) return exit(0);
    int a1, a2, c1, c2;
    for(int i = 1; i <= m; i++) {
        read(a1, a2, c1, c2);
        a1++, a2++;
        int u1 = a1 + c1 * n, u2 = a1 + (1 - c1) * n;
        int v1 = a2 + c2 * n, v2 = a2 + (1 - c2) * n;
        G.AddEdge(u1, v2); G.AddEdge(v1, u2);
    }
}

int dfn[N << 1], low[N << 1], cntd;
int clb[N << 1], vis[N << 1], cntc;
stack<int >st;

inline void Tarjan(int u) {
    dfn[u] = low[u] = ++cntd;
    vis[u] = 1; st.push(u);
    for(int i = G.head(u); i; i = G.nt(i)) {
        int v = G.to(i);
        if(!dfn[v]) {
            Tarjan(v);
            low[u] = min(low[u], low[v]);
        }
        else if(vis[v]) {
            low[u] = min(low[u], dfn[v]);
        }
    }
    if(low[u] == dfn[u]) {
        cntc++; int tmp;
        do {
            tmp = st.top(); 
            st.pop();
            clb[tmp] = cntc;
            vis[tmp] = 0;
        }while(tmp != u);
    }
}

inline void Work() {
    for(int i = 1; i <= 2 * n; i++) {
        if(!dfn[i]) Tarjan(i);
    }
    int flag = 1;
    for(int i = 1; i <= n; i++) {
        if(clb[i] == clb[i + n]) {
            flag = 0;
            break;
        }
    }
    if(flag) printf("YES\n");
    else printf("NO\n");
}

inline void Clear() {
    cntd = 0, cntc = 0;
    G.clear();
    memset(clb, 0, sizeof(clb));
    memset(dfn, 0, sizeof(dfn));
    memset(vis, 0, sizeof(vis));
    while(!st.empty()) st.pop();
}

int main() {
    int T = -1;
    while(~scanf("%d%d", &n, &m)) {
        Input();
        Work();
        Clear();
    }
    return 0;
}

算法细节：小小的承诺

  • SAT 问题的细节

关于 2-SAT 其实就是一些对于特殊情况建立边的内容了。一定要谨记，2-SAT 所连的边一定是不得不连的，比如说对于两个二元组 $(x_0,x_1),(y_0,y_1)$，其中这个元素代表的值和它的下表一样。我们强制要求选择出来的值的或运算结果为 $1$。那么这时候我们就没有 $x_1,y_1$ 向另外两点连边的需要，因为这两个已经是 $1$，剩下的不管怎么选都是 $1$。只需要对于 $x_0,y_0$ 这一类点来连边即可。

算法实战：长久的陪伴

查看相关算法标签喵！

参考资料（以下排名不分先后）