2-SAT

什么是 2-SAT ？

SAT 是 Satisfiability 的缩写，意为可满足性。
n-SAT 问题即对一串 bool 变量进行赋值，满足 n 元 bool 方程组。
当 $n\ge3$ 时，n-SAT 问题已被证明是NP完全的，暂时没有多项式复杂度的做法；
但今天的主角 2-SAT 是可以在线性时间复杂度内解决的。

如何求解 2-SAT 问题？

转化为图论问题。
具体的，对于每个变量 $x$ ，我们建立两个点 $x$ 与 $\neg x$ ，分别表示 $x$ 取 true 或 false 。对于每个要求 $(a\vee b)$ ，连接 $\neg a \to b$ 和 $\neg b\to a$ ，表示“ $a$ 为假 $b$ 必为真，$b$ 为假 $a$ 必为真”。

建好图后，我们发现若点 $x$ 为真，则点 $x$ 可到达的点必然都为真。显然的，若点 $x$ 与 $\neg x$ 可互达，此问题必然无解，毕竟一个值不可能同时即为真又为假 $\tiny{\text{薛定谔的bool（不是）}}$ 。稍作思考后，我们发现同一 强连通分量 内的点的值必然相等，因为均可互达。

到这里，我们就可以愉快的缩点啦！
顺带一提，缩点我使用了 $kosaraju$ 算法，因为这样缩出的点已经按拓扑序排序，而 $tarjan$ 求出的是逆拓扑序的。

$\texttt{code}$
$\small\text{大量使用三目运算符，极度不适}$

void add(int x, int y) { g[x].push_back(y), r[y].push_back(x); }
void dfs1(int x) {
    vis[x] = true;
    for (auto i : g[x]) !vis[i] ? dfs1(i) : void();
    s.push_back(x);
}
void dfs2(int x) {
    bel[x] = cnt;
    for (auto i : r[x]) !bel[i] ? dfs2(i) : void();
}
void kosaraju() {
    for (int i = 1; i <= n << 1; i++) !vis[i] ? dfs1(i) : void();
    for (auto i = s.rbegin(); i != s.rend(); i++) !bel[*i] ? cnt++, dfs2(*i) : void();
}

缩点之后，如何得出每个点的取值呢？

我们有以下结论：一定选择拓扑序更大的。

考虑证明。设变量 $x_i$ 对应的节点为 $u_{i,p}\ ,p\in \{0,1\}$

引理

根据建图规则，若存在边 $(u_{i,p},u_{j,q})$ ，则必然存在边 $(u_{j,q\ \text{xor}\ 1},u_{i,p\ \text{xor}\ 1})$ 。
更进一步的，若存在路径 $(u_{i,p},u_{j,q})$ ，必然存在路径 $(u_{j,q\ \text{xor}\ 1},u_{i,p\ \text{xor}\ 1})$ 。

证明

考虑反证法。
记 $f(u_{i,p})$ 表示点 $u_{i,p}$ 缩点后所在点的拓扑序。

设有 $f(u_{i,p})>f(u_{i,p\ \text{xor}\ 1})$ ， $f(u_{j,q})<f(u_{j,q\ \text{xor}\ 1})$ 且存在路径 $(u_{i,p},u_{j,q})$ ，这样由我们的算法会得出错误结果。

然而，因为存在路径 $(u_{i,p},u_{j,q})$ ，所以 $f(u_{i,p})\le f(u_{j,q})$ ；存在路径 $(u_{i,p},u_{j,q})$ ，故存在路径 $(u_{j,q\ \text{xor}\ 1},u_{i,p\ \text{xor}\ 1})$ ，所以 $f(u_{j,q\ \text{xor}\ 1})\le f(u_{i,p\ \text{xor}\ 1})$ 。联立后，明显产生矛盾，说明这种情况不存在。
$\tiny\text{算是证毕了吧？}$

洛谷P4782 【模板】2-SAT 问题

$\texttt{code}$

#include <bits/stdc++.h>
using namespace std;
int n, m, bel[2000010], cnt;
vector<int> g[2000010], r[2000010], s;
bool vis[2000010];
void add(int x, int y) { g[x].push_back(y), r[y].push_back(x); }
void dfs1(int x) {
    vis[x] = true;
    for (auto i : g[x]) !vis[i] ? dfs1(i) : void();
    s.push_back(x);
}
void dfs2(int x) {
    bel[x] = cnt;
    for (auto i : r[x]) !bel[i] ? dfs2(i) : void();
}
void kosaraju() {
    for (int i = 1; i <= n << 1; i++) !vis[i] ? dfs1(i) : void();
    for (auto i = s.rbegin(); i != s.rend(); i++) !bel[*i] ? cnt++, dfs2(*i) : void();
}
int main() {
    scanf("%d%d", &n, &m);
    while (m--) {
        int a, b, c, d;
        scanf("%d%d%d%d", &a, &b, &c, &d);
        add(a + !b * n, c + d * n), add(c + !d * n, a + b * n);
    }
    kosaraju();
    for (int i = 1; i <= n; i++)
        if (bel[i] == bel[i + n]) {
            printf("IMPOSSIBLE\n");
            return 0;
        }
    printf("POSSIBLE\n");
    for (int i = 1; i <= n; i++) {
        printf("%d ", bel[i] < bel[i + n]);
    }
    return 0;
}