2-SAT提高组

💡 核心思想

2-SAT（2-Satisfiability）是判断布尔方程组是否有解的问题。每个方程限制两个布尔变量的关系（如 a ∨ b，¬a ∨ c）。核心思想是：将每个变量 x 拆分为两个节点 x（真）和 ¬x（假），每个限制条件转化为两条有向边（蕴含关系）。然后求强连通分量（SCC），如果某个变量和它的否定在同一个 SCC 中，则无解；否则，按拓扑序的逆序确定变量取值。

🎯 直觉理解

想象你在安排一个活动，每个人有两个可选时间（上午或下午），但有些人不能同时在同一个时间。2-SAT 就是帮你判断"是否存在一个让所有人都满意的安排"。它把"如果 A 选上午，那么 B 必须选下午"这样的约束画成一张有向图，然后看看图中有没有"自相矛盾"的环。

📝 算法流程

1. 每个布尔变量 x 拆成两个节点：x（真，编号 2x）和 ¬x（假，编号 2x+1）
2. 对每个约束 a ∨ b，添加两条边：¬a → b 和 ¬b → a
3. 对图求强连通分量（Tarjan / Kosaraju）
4. 检查：如果 x 和 ¬x 在同一 SCC，则无解
5. 否则，按 SCC 的拓扑序逆序赋值：如果 x 的 SCC 编号 > ¬x 的，则 x = true

$$a \lor b \equiv \neg a \to b \equiv \neg b \to a$$

$$\text{有解} \Leftrightarrow \forall x, \text{ x 和 } \neg x \text{ 不在同一 SCC}$$

📊 复杂度分析

💻 参考实现（C++）

#include 
using namespace std;

// 2-SAT 模板
struct TwoSAT {
    int n;
    vector> g;
    vector dfn, low, scc, stk;
    vector inStk;
    int timer, sccCnt;
    
    TwoSAT(int n) : n(n), g(2 * n) {}
    
    // x = valX 或 y = valY 必须满足一个
    void addOr(int x, bool valX, int y, bool valY) {
        g[2 * x + !valX].push_back(2 * y + valY);
        g[2 * y + !valY].push_back(2 * x + valX);
    }
    
    void tarjan(int u) {
        dfn[u] = low[u] = ++timer;
        stk.push_back(u); inStk[u] = true;
        for (int v : g[u]) {
            if (!dfn[v]) { tarjan(v); low[u] = min(low[u], low[v]); }
            else if (inStk[v]) low[u] = min(low[u], dfn[v]);
        }
        if (dfn[u] == low[u]) {
            sccCnt++;
            while (true) {
                int x = stk.back(); stk.pop_back();
                inStk[x] = false; scc[x] = sccCnt;
                if (x == u) break;
            }
        }
    }
    
    bool solve(vector& ans) {
        dfn.resize(2 * n); low.resize(2 * n); scc.resize(2 * n);
        inStk.resize(2 * n); timer = sccCnt = 0;
        for (int i = 0; i < 2 * n; i++) if (!dfn[i]) tarjan(i);
        
        ans.resize(n);
        for (int i = 0; i < n; i++) {
            if (scc[2 * i] == scc[2 * i + 1]) return false;
            ans[i] = scc[2 * i] > scc[2 * i + 1];
        }
        return true;
    }
};

int main() {
    TwoSAT ts(3);
    // x0 = true 或 x1 = false
    ts.addOr(0, true, 1, false);
    // x1 = true 或 x2 = true
    ts.addOr(1, true, 2, true);
    
    vector ans;
    if (ts.solve(ans)) {
        for (bool x : ans) cout << (x ? "T " : "F ");
        cout << endl;
    } else {
        cout << "IMPOSSIBLE" << endl;
    }
    return 0;
}

⚠️ 常见坑点

📚 相关题目