2-SAT

SAT（Satisfiability）即适定性问题。一般形式为 k-SAT，当 $k > 2$ 时该问题是 NP 完全的。2-SAT 是指每个限制条件只涉及两个变量的适定性问题，可以在线性时间内求解。

定义

2-SAT 问题通常给定 $n$ 个布尔变量 $x_1, x_2, \dots, x_n$ 以及 $m$ 个限制条件。每个条件形如 $x_i = v_i \lor x_j = v_j$，即变量 $x_i$ 取值 $v_i$ 或变量 $x_j$ 取值 $v_j$ 至少有一个满足（其中 $v_i, v_j \in \{0, 1\}$）。目标是为每个变量找出一组赋值，使得所有条件同时满足。

解决思路

2-SAT 问题的核心是将逻辑限制转化为有向图中的含义（含义即“如果 A 则 B”）。

对于一个限制 $A \lor B$，它等价于：

• 如果 $\neg A$ 成立，则 $B$ 必须成立。
• 如果 $\neg B$ 成立，则 $A$ 必须成立。

建图方法

对于每个布尔变量 $x_i$，我们建立两个节点：$x_i$ 表示 $x_i$ 为真，$\neg x_i$ 表示 $x_i$ 为假。通常可以用 $i$ 表示真，$i + n$ 表示假。

根据限制条件 $x_i = v_i \lor x_j = v_j$，我们可以建立两条有向边：

• $\neg (x_i = v_i) \to (x_j = v_j)$
• $\neg (x_j = v_j) \to (x_i = v_i)$

常见的逻辑关系转化如下表：

逻辑关系	转化为命题	建立的有向边
$x_i \lor x_j$	$\neg x_i \to x_j, \neg x_j \to x_i$	$i+n \to j, j+n \to i$
$\neg x_i \lor x_j$	$x_i \to x_j, \neg x_j \to \neg x_i$	$i \to j, j+n \to i+n$
$x_i$ 必须为真	$x_i \lor x_i$	$i+n \to i$

求解算法

利用强连通分量（SCC）可以高效解决 2-SAT 问题。

1. 找强连通分量：对建立的有向图运行 Tarjan 算法。
2. 判断可行性：对于任意变量 $x_i$，如果 $x_i$ 和 $\neg x_i$ 位于同一个 SCC 中，则说明存在 $x_i \to \dots \to \neg x_i \to \dots \to x_i$ 的矛盾路径，此时问题无解。
3. 确定赋值：如果问题有解，我们可以通过 SCC 的编号确定一组可行解。在 Tarjan 算法中，SCC 编号的顺序实际上是 反拓扑序。
   • 如果 scc[x_i] < scc[\neg x_i]，则取 $x_i$ 为真（因为 $x_i$ 在缩点后的 DAG 中位置更靠后）。
   • 否则取 $x_i$ 为假。

实现 (C++)

#include <vector>
#include <stack>
#include <algorithm>

using namespace std;

struct TwoSAT {
    int n;
    vector<vector<int>> adj;
    vector<int> dfn, low, scc;
    vector<bool> in_stack;
    stack<int> st;
    int timestamp, scc_cnt;

    // n 为变量个数，节点范围 1..2n
    // 1..n 表示真，n+1..2n 表示假
    TwoSAT(int n) : n(n), adj(2 * n + 1), dfn(2 * n + 1, 0), 
                    low(2 * n + 1, 0), scc(2 * n + 1, 0), 
                    in_stack(2 * n + 1, false), timestamp(0), scc_cnt(0) {}

    // 添加限制：x_i 为 a 或 x_j 为 b
    // a, b 为布尔值 (0/1)
    void add_clause(int i, bool a, int j, bool b) {
        // x_i = !a => x_j = b
        // x_j = !b => x_i = a
        int u = i + (a ? 0 : n);
        int v = j + (b ? 0 : n);
        int not_u = i + (a ? n : 0);
        int not_v = j + (b ? n : 0);
        adj[not_u].push_back(v);
        adj[not_v].push_back(u);
    }

    void tarjan(int u) {
        dfn[u] = low[u] = ++timestamp;
        st.push(u);
        in_stack[u] = true;

        for (int v : adj[u]) {
            if (!dfn[v]) {
                tarjan(v);
                low[u] = min(low[u], low[v]);
            } else if (in_stack[v]) {
                low[u] = min(low[u], dfn[v]);
            }
        }

        if (dfn[u] == low[u]) {
            scc_cnt++;
            while (true) {
                int v = st.top();
                st.pop();
                in_stack[v] = false;
                scc[v] = scc_cnt;
                if (u == v) break;
            }
        }
    }

    bool solve(vector<bool>& result) {
        for (int i = 1; i <= 2 * n; ++i) {
            if (!dfn[i]) tarjan(i);
        }

        for (int i = 1; i <= n; ++i) {
            if (scc[i] == scc[i + n]) return false;
            result[i] = (scc[i] < scc[i + n]);
        }
        return true;
    }
};

总结

2-SAT 是将逻辑问题转化为图论问题的经典案例。理解其核心在于利用强连通分量处理逻辑含义中的传递性。在实现时，注意节点编号与布尔值的对应关系，以及 Tarjan 算法得到的 SCC 编号与拓扑序的对应关系。