( m 2-sat) 问题指的是一类需要给 (n) 个变量赋值真假然后满足 (m) 条形如 (a ightarrow true / false) 或 (b ightarrow true / false) 限制的问题。
首先可以发现的是，这个问题显得极为抽象，因此将这个抽象问题具体化是一个不赖的选择。
那么可以考虑将这个问题在图上以一种直观的形式表现出来。
又因为要体现出每个变量有两种取值，因此可以考虑将每个变量拆成 (2) 个点，分别表示真/假。
下面我们要做的就是将这 (m) 条限制在图上表达出来，因为是点与点之间的关系，因此用边代表限制是必然的。
考虑一个具体的例子，(a ightarrow true) 或 (b ightarrow true) 怎么表示出来。
如果 (a) 为真，我们考虑从 (a) 连出去一条边，那么只能同时连到 (b) 对应的两个点表示在 (a) 为真的前提下 (b) 为真或 (b) 为假对 (b) 类似。
但是这样的连边方式使得限制条件变得宽松，在图上并不能起到任何作用，那么就需要换一种表示方式。
相反地，我们考虑如果 (a) 为假，那么 (b) 就必须为真，这样的限制就非常紧了。
因此我们从 (a) 为假向 (b) 为真连一条边，对 (b) 类似，同时对其他几种限制条件也类似。
这样一来你会发现，我们可以找出无解的一个必要条件：
- 对于任意一个变量 (x) 如果 (x) 为真与 (x) 为假存在于一个强连通分量中那么就无解。
原因很简单，因为同一个强连通分量内部所有点的选择状态必须是相同的，运用反证法不难证明。
所以如果 (x) 的两个状态存在于一个强连通分量内，那么这两个状态要么同时成立，要么同时不成立，这是不可能的，因此此时这个问题无解。
那么这是不是 ( m 2-sat) 问题有解的充要条件呢？
答案是正确的，下面我们考虑构造出一种合法的解。
因为同一强连通分量内所有点的选择状态都是相同的，因此我们不妨直接将这张图缩点变成一张 ( m DAG) 方便处理。
你会发现如果一个点 (x) 为真，那么 (x) 往后能走到的所有点都必须为真。
那么如果选择让其为真的强连通分量在拓扑序上越靠前就越难造出一组解，因此我们贪心地让拓扑序大的强连通分量为真。
那么对于每个变量 (x)，我们考察其两个状态所在强连通分量的拓扑序，让拓扑序大的哪个强连通分量为真。
但你会发现这样一个问题，如果出现了 (a ightarrow lnot a ightarrow b ightarrow lnot b) 的这样一条有向路径呢？
仔细分析，这样的路径应该是不存在的。
首先，根据定义 (a) 可以通过一条路径走到 (lnot a)。
其次，当从 (lnot a) 向外连向 (v) 时，(lnot v) 必然也会连向 (a)，这样最终一定会存在 (lnot a ightarrow b, lnot b ightarrow a) 这样的两条路径。
根据定义 (b) 可以走到 (lnot b)，因此 (lnot a) 可以走到 (a) 同时 (a) 可以走到 (lnot a)，因此 (a, lnot a) 在同一个强连通分量内，矛盾。
只要一条路径上存在至少两对相同变量的两个状态，都可以用类似的方式证明。
所以一条路径上至多存在一对相同变量的两个状态，因此上面贪心的构造方法是正确的。
#include <bits/stdc++.h>
using namespace std;
#define rep(i, l, r) for (int i = l; i <= r; ++i)
#define Next(i, u) for (int i = h[u]; i; i = e[i].next)
const int N = 2000000 + 5;
struct egde { int v, next;} e[N];
int n, m, u, v, a, b, tot, cnt, col, top, h[N], co[N], st[N], dfn[N], low[N];
int read() {
char c; int x = 0, f = 1;
c = getchar();
while (c > '9' || c < '0') { if(c == '-') f = -1; c = getchar();}
while (c >= '0' && c <= '9') x = x * 10 + c - '0', c = getchar();
return x * f;
}
int c(int x, int sta) { return x + n * (sta & 1);}
void add(int u, int v) { e[++tot].v = v, e[tot].next = h[u], h[u] = tot; }
void tarjan(int u) {
dfn[u] = low[u] = ++cnt, st[++top] = u;
Next(i, u) {
int v = e[i].v;
if(!dfn[v]) tarjan(v), low[u] = min(low[u], low[v]);
else if(!co[v]) low[u] = min(low[u], dfn[v]);
}
if(dfn[u] == low[u]) {
co[u] = ++col;
for (; st[top] != u; --top) co[st[top]] = col;
--top;
}
}
int main() {
n = read(), m = read();
rep(i, 1, m) {
u = read(), a = read(), v = read(), b = read();
add(c(u, a ^ 1), c(v, b)), add(c(v, b ^ 1), c(u, a));
}
rep(i, 1, 2 * n) if(!dfn[i]) tarjan(i);
rep(i, 1, n) if(co[i] == co[i + n]) { puts("IMPOSSIBLE"); return 0;}
puts("POSSIBLE");
rep(i, 1, n) printf("%d ", (co[i] > co[i + n]));
return 0;
}
值得一提的是，具体问题抽象化在这个问题中扮演者不可或缺的角色，同时我们要尽可能将判定条件收紧而不是放松。
往往任何一个判定性问题通常我们可以找到一些必要条件，然后通过这些必要条件构造出一组合法解。