介绍2-SAT问题及其解决方法。

        SAT问题即Satisfiability（可满足性问题），是指对一串布尔变量，对其进行赋值，使之满足布尔方程的问题。对于每一个约束条件，我们可以将它们写成布尔表达式的形式。比如对于布尔变量$a、b$，布尔表达式$¬a∨b$就是一个约束条件，它的意思是要求a为假或者b为真。
        如果每一个约束条件只有两个条件（如同上文举的例子），则称其为2-SAT问题，它可以抽象为图，用图论的方式去解决。
        对于约束条件$a∨b$，它的意思是a为真或者b为真，这个式子也可以理解成$\lnot a\rightarrow b ∧ \lnot b \rightarrow a$，显然两个式子是等价的。这时我们可以将变量抽象为点，$\rightarrow$引导的关系抽象为有向边，建立有向图。由于取非的存在，顶点数扩大一倍，我们通常用x+n来表示x的取反形式。
        建完图之后，容易发现同一个强连通分量中的点其真值必然是相同的。因此如果一个变量及其取反形式在同一个强连通分量中，该问题无解。
        那对于有解的情况，如何确定答案？对有向图tarjan强连通缩点后进行拓扑排序，对于每一个变量，我们认为拓扑序靠后的一个真值为真，靠前的一个为假。比如$\lnot x$拓扑序靠后，其真值为真，因此我们判定$x$为假。这样做的好处是不会出现自相矛盾的情况，重复这个步骤就可以得到一组特解。注意这种方法不能得到全部的解。算法时间复杂度为线性时间复杂度。
        模板题：戳这里。
        下面给出示例代码，这里利用tarjan缩点本身可以得到反拓扑序相对顺序这一特点省略了拓扑排序过程。

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
#include<bits/stdc++.h>

#define N 1000005
using namespace std;
struct Edge {
    int next, to;
} edge[N << 1];
int head[N << 1], cnt = 1, n, m, color[N << 1], DFN[N << 1], LOW[N << 1], in = 1, ID = 1, vis[N << 1];

inline void add(int x, int y) {
    edge[cnt].to = y, edge[cnt].next = head[x], head[x] = cnt++;
}

inline int read() {
    char e = getchar();
    int s = 0;
    while (e < '-')e = getchar();
    while (e > '-')s = (s << 1) + (s << 3) + (e & 15), e = getchar();
    return s;
}

stack<int> sta;

void tarjan(int x) {//tarjan算法过程
    if (DFN[x])return;
    DFN[x] = LOW[x] = in++, vis[x] = 1, sta.push(x);
    for (int i = head[x]; i; i = edge[i].next) {
        if (vis[edge[i].to])LOW[x] = min(DFN[edge[i].to], LOW[x]);
        else if (!DFN[edge[i].to])tarjan(edge[i].to), LOW[x] = min(LOW[x], LOW[edge[i].to]);
    }
    if (DFN[x] == LOW[x]) {
        int t;
        do color[t = sta.top()] = ID, vis[t] = 0, sta.pop();
        while (t != x);
        ID++;
    }
}

int main() {
    n = read(), m = read();
    for (int i = 1; i <= m; i++) {
        int a = read(), b = read(), c = read(), d = read();
        if (b && d)add(a + n, c), add(c + n, a);//建图
        else if ((!b) && d)add(a, c), add(c + n, a + n);
        else if (b)add(a + n, c + n), add(c, a);
        else add(a, c + n), add(c, a + n);
    }
    for (int i = 1; i <= (n << 1); i++)tarjan(i);//tarjan缩点
    for (int i = 1; i <= n; i++) {
        if (color[i] == color[i + n]) {//在同一个强连通分量中无解
            cout << "IMPOSSIBLE";
            return 0;
        }
    }
    cout << "POSSIBLE" << endl;
    for (int i = 1; i <= n; i++) {
        if (color[i] < color[i + n])cout << "1 ";//注意是反拓扑序
        else cout << "0 ";
    }
    return 0;
}