SAT是是适定性（Satisfiability）问题的简称。一般形式为 k - 适定性问题，简称 k-SAT。而当\(k>2\)时该问题为 NP 完全的。

定义

有 \(n\) 个布尔变量 \(x_1\)\(\sim\)\(x_n\)，另有 \(m\) 个需要满足的条件，每个条件的形式都是 「\(x_i\) 为 true / false 或 \(x_j\) 为 true / false」。比如 「\(x_1\) 为真或 \(x_3\) 为假」、「\(x_7\) 为假或 \(x_2\) 为假」。

注意这里的或为排斥或

2-SAT 问题的目标是给每个变量赋值使得所有条件得到满足。

Tarjan SCC 缩点

把每个变量拆成两个点，\(X(True)\)和\(X(False)\)。比如现在有一个要求\(X|Y=True\)，则把\(X(False)\)到\(Y(True)\)连一条边，把\(X(True)\)到\(Y(False)\)连一条边。连出来的图是对称的，然后跑一遍 Tarjan，如果存在某个变量的两个点在同一个强连通分量中的情况，则无解，否则有解。

构造方案时，我们可以通过缩点后的拓扑序确定变量的值。如果变量\(x\)的拓扑序在\(\neg x\)之后，则取\(x\)为真，反之取\(x\)为假。注意 Tarjan 求得的 SCC 的编号相同与反拓扑序。

// luogu P4782
int32_t main() {
    int n, m, N;
    cin >> n >> m, N = n * 2 + 2;
    e.resize(N);
    dfn = inStk = low = scc = vector<int>(N);
    capacity.push_back(0);
    for (int i, a, j, b; m; m--) {
        cin >> i >> a >> j >> b;
        e[2 * i + (a ^ 1)].push_back(2 * j + b);
        e[2 * j + (b ^ 1)].push_back(2 * i + a);
    }
    for (int i = 2; i <= n * 2 + 1; i++)
        if (!dfn[i])
            tarjan(i);
    vector<int> res(n + 1);
    for (int i = 1; i <= n; i++) {
        if (scc[i * 2] == scc[i * 2 + 1])
            cout << "IMPOSSIBLE\n", exit(0);
        else if (scc[i * 2] > scc[i * 2 + 1])
            res[i] = 1;
    }
    cout << "POSSIBLE\n";
    for (int i = 1; i <= n; i++)
        cout << res[i] << " ";
    cout << "\n";
    return 0;
}