\(\rm 2-sat\) 問題指的是一類需要給 \(n\) 個變數賦值真假然後滿足 \(m\) 條形如 \(a \rightarrow true / false\) 或 \(b \rightarrow true / false\) 限制的問題。

首先可以發現的是，這個問題顯得極為抽象，因此將這個抽象問題具體化是一個不賴的選擇。

那麼可以考慮將這個問題在圖上以一種直觀的形式表現出來。

又因為要體現出每個變數有兩種取值，因此可以考慮將每個變數拆成 \(2\) 個點，分別表示真/假。

下面我們要做的就是將這 \(m\) 條限制在圖上表達出來，因為是點與點之間的關係，因此用邊代表限制是必然的。

考慮一個具體的例子，\(a \rightarrow true\)

如果 \(a\) 為真，我們考慮從 \(a\) 連出去一條邊，那麼只能同時連到 \(b\) 對應的兩個點表示在 \(a\) 為真的前提下 \(b\) 為真或 \(b\) 為假對 \(b\) 類似。

但是這樣的連邊方式使得限制條件變得寬鬆，在圖上並不能起到任何作用，那麼就需要換一種表示方式。

相反地，我們考慮如果 \(a\) 為假，那麼 \(b\) 就必須為真，這樣的限制就非常緊了。

因此我們從 \(a\) 為假向 \(b\) 為真連一條邊，對 \(b\) 類似，同時對其他幾種限制條件也類似。

這樣一來你會發現，我們可以找出無解的一個必要條件：

• 對於任意一個變數 \(x\) 如果 \(x\) 為真與 \(x\) 為假存在於一個強連通分量中那麼就無解。

原因很簡單，因為同一個強連通分量內部所有點的選擇狀態必須是相同的，運用反證法不難證明。

所以如果 \(x\) 的兩個狀態存在於一個強連通分量內，那麼這兩個狀態要麼同時成立，要麼同時不成立，這是不可能的，因此此時這個問題無解。

那麼這是不是 \(\rm 2-sat\) 問題有解的充要條件呢？

答案是正確的，下面我們考慮構造出一種合法的解。

因為同一強連通分量內所有點的選擇狀態都是相同的，因此我們不妨直接將這張圖縮點變成一張 \(\rm DAG\) 方便處理。

你會發現如果一個點 \(x\)

那麼如果選擇讓其為真的強連通分量在拓撲序上越靠前就越難造出一組解，因此我們貪心地讓拓撲序大的強連通分量為真。

那麼對於每個變數 \(x\)，我們考察其兩個狀態所在強連通分量的拓撲序，讓拓撲序大的哪個強連通分量為真。

但你會發現這樣一個問題，如果出現了 \(a \rightarrow \lnot a \rightarrow b \rightarrow \lnot b\) 的這樣一條有向路徑呢？

仔細分析，這樣的路徑應該是不存在的。

首先，根據定義 \(a\) 可以通過一條路徑走到 \(\lnot a\)。

其次，當從 \(\lnot a\) 向外連向 \(v\) 時，\(\lnot v\) 必然也會連向 \(a\)，這樣最終一定會存在 \(\lnot a \rightarrow b, \lnot b \rightarrow 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;
}

值得一提的是，具體問題抽象化在這個問題中扮演者不可或缺的角色，同時我們要儘可能將判定條件收緊而不是放鬆。

往往任何一個判定性問題通常我們可以找到一些必要條件，然後通過這些必要條件構造出一組合法解。