SAT 是适定性 \(\text{(Satisfiability)}\) 问题的简称。一般形式为 k - 适定性问题，简称 k-SAT。而当 \(k>2\) 时该问题为 NP 完全的。所以我们只研究 \(k=2\) 的情况。
2-SAT，简单的说就是给出 \(n\) 个集合，每个集合有两个元素，已知若干个 \(<a,b>\)，表示 \(a\) 与 \(b\) 矛盾（其中 \(a\) 与 \(b\) 属于不同的集合）。然后从每个集合选择一个元素，判断能否一共选 \(n\) 个两两不矛盾的元素。显然可能有多种选择方案，一般题中只需要求出一种即可。
建图
我们将 \(n\) 个集合拆成两个点，分别代表着 true 和 false.
当 a || b == true 时，我们可以得知：
a == false 时，b = true；
b == false 时，a = true;
这两个关系存在因果关系；
而 a == true 时，我们不能得知 b = true 还是 b = false，这两者之间不存在因果关系，b == true 同理。
因此，我们将 \(a_0\) 向 \(b_1\) 连边，将 \(b_0\) 向 \(a_1\) 连边。
含义：
当a == false时，b = true；
当b == false时，a = true。
当 a && b == false 时，我们可以得知：
a == true 时，b = false;
b == true 时，a = false;
我们将 \(a_1\) 向 \(b_0\) 连边，将 \(b_1\) 向 \(a_0\) 连边。
含义：
当a == true时，b = false;
当b == true时，a = false。
当 a && b == true 时，我们发现，a == true，b == true，除了这种情况不会再有其他情况了，即 \(a\) 的值一定为 true，\(b\) 的值一定为 true。
这种情况下，我们将 \(a_0\) 向 \(a_1\) 连边，\(b_0\) 向 \(b_1\) 连边。
含义：
当a == false时，a = true;（即 \(a\) 一定不为false）
当b == false时，b = true。(即 \(b\) 一定不为true)
判断是否有解
如果 \(a_0\) 可以到达 \(a_1\)，说明 \(a\) 一定为 true；
如果 \(a_1\) 可以到达 \(a_0\)，说明 \(a\) 一定为 false。
判断是否有解即在一种情况中 \(a\) 都有唯一确定的值，要么为 true，要么为 false，倘若在同一种情况中，\(a_0\) 可以到达 \(a_1\)， \(a_1\) 可以到达 \(a_0\)，则无法确定 \(a\) 的值，此情况下无解，即 \(a_0\) 与 \(a_1\) 在同一个强连通分量里。
用 tarjan 算法来找强连通分量即可。
题目
#include <bits/stdc++.h>
using namespace std;
typedef long long ll;
const int N = 1e6 + 5;
int n, m, tim, scc;
vector<int> son[N << 1], sta;
int dfn[N << 1], low[N << 1], lt[N << 1];
void tarjan(int u) {
dfn[u] = low[u] = ++ tim;
sta.push_back(u);
for (int v : son[u]) {
if (!dfn[v]) {
tarjan(v);
low[u] = min(low[u], low[v]);
}
else if (!lt[v]) {
low[u] = min(low[u], dfn[v]);
}
}
if (dfn[u] == low[u]) {
lt[u] = ++ scc;
while (sta.back() != u) {
lt[sta.back()] = scc;
sta.pop_back();
}
sta.pop_back();
}
}
int main() {
scanf("%d%d", &n, &m);
while (m --) {
int xi, i, xj, j;
scanf("%d%d%d%d", &xi, &i, &xj, &j);
son[xi + n * (i & 1)].push_back(xj + (j ^ 1) * n);
son[xj + n * (j & 1)].push_back(xi + (i ^ 1) * n);
}
for (int i = 1; i <= (n << 1); ++ i) {
if (!dfn[i]) {
tarjan(i);
}
}
for (int i = 1; i <= n; ++ i) {
if (lt[i] == lt[i + n]) {
puts("IMPOSSIBLE");
return 0;
}
}
puts("POSSIBLE");
for (int i = 1; i <= n; ++ i) {
printf("%d%c", (lt[i] < lt[i + n]), " \n"[i == n]);
}
return 0;
}