In-Depth Analysis of 2-SAT Problem: Efficient Solutions B...

Core Logic and Mathematical Principles

Topological sorting plays a crucial role in the algebraic construction for solving the construction problem of 2-SAT (2-Satisfiability).

The goal of the 2-SAT problem is: given $N$ Boolean variables $x_1, x_2, \dots, x_n$, and $M$ constraints, each of which is in the form "either $x_i$ is true or $x_j$ is true" ($x_i \lor x_j$). We need to assign truth values (0 or 1) to each variable such that all conditions are satisfied simultaneously.

1. Algebraic Isomorphism from Propositional Logic to Directed Graphs (Implication Graphs)

According to the equivalent transformations of logical algebra, a disjunctive condition $A \lor B$ is mathematically equivalent to two implications:

$$\neg A \implies B \quad \text{and} \quad \neg B \implies A$$

Physical Essence: This means "if $A$ does not hold, then $B$ must hold"; similarly, "if $B$ does not hold, then $A$ must hold".
Implication Graph Construction: We split each variable $x_i$ into two independent topological nodes: $i$ (representing $x_i$ is true) and $i + n$ (representing $x_i$ is false, i.e., $\neg x_i$). For each constraint, we draw two directed edges in the graph. This graph containing $2N$ nodes is called the implication graph.

2. Legitimacy Criterion for Strongly Connected Components (SCC)

Utilizing Tarjan's algorithm or Kosaraju's algorithm to compress the strongly connected components of the implication graph:

No-Solution Criterion: If in the final topological space, there exists any variable $x_i$, whose corresponding positive state $i$ and negative state $i + n$ belong to the same strongly connected component ($\text{scc}[i] == \text{scc}[i+n]$), it algebraically implies $x_i \implies \neg x_i$ and $\neg x_i \implies x_i$, leading to a logical contradiction, thus determining that the 2-SAT problem has no global solution.

3. Greedy Consistent Assignment Driven by Reverse Topological Order

Once a solution is determined, how do we construct a specific valid solution?

Reverse Topological Selection Principle: The strongly connected component numbers obtained from Tarjan's algorithm (the scc array) naturally satisfy the reverse topological order (the smaller the number, the closer it is to the leaf sink in the topological graph).
Decision Tree Consolidation: If there exists a directed path $u \implies v$, if we choose $u$ to be true, then we must forcibly choose $v$ to be true. Due to the chain contamination of logical implications, when constructing solutions, we should prioritize selecting nodes that are further back in the topological sequence (i.e., closer to the front in the reverse topological order) as true values, minimizing subsequent constraints.
Constructing Conclusions: For each variable $x_i$:
- If $\text{scc}[i] < \text{scc}[i+n]$, it indicates that in the forward topological order, the negative state $i+n$ is behind. According to the greedy strategy, assign $x_i$ to false (0).
- If $\text{scc}[i] > \text{scc}[i+n]$, it indicates that in the forward topological order, the positive state $i$ is behind. Assign $x_i$ to true (1).

Algorithm Derivation and State Design

1. Implication Graph State Design

For variable $i \in [1, n]$:

Node $i$ represents $x_i = \text{true}$
Node $i + n$ represents $x_i = \text{false}$

Common constraint transformations:

$x_i \lor x_j$ (at least one is true): $\neg x_i \implies x_j$ and $\neg x_j \implies x_i$. Edges: add_edge(i + n, j), add_edge(j + n, i).
$x_i \implies x_j$ (if $i$ is true, then $j$ must be true): Edges: add_edge(i, j), add_edge(j + n, i + n).
$x_i$ must be true: equivalent to $x_i \lor x_i$. Edge: add_edge(i + n, i).

C++ Standard Source Code (High-Precision Template for 2-SAT Construction)

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

const int MAXN = 200005; // 2 * N space base

std::vector<int> adj[MAXN * 2];
int dfn[MAXN * 2], low[MAXN * 2], scc[MAXN * 2];
bool in_stack[MAXN * 2];
std::stack<int> stk;
int timer = 0, scc_cnt = 0;

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

    for (size_t i = 0; i < adj[u].size(); ++i) {
        int v = adj[u][i];
        if (!dfn[v]) {
            tarjan(v);
            low[u] = std::min(low[u], low[v]);
        } else if (in_stack[v]) {
            low[u] = std::min(low[u], dfn[v]);
        }
    }

    if (low[u] == dfn[u]) {
        scc_cnt++;
        while (true) {
            int v = stk.top();
            stk.pop();
            in_stack[v] = false;
            scc[v] = scc_cnt; // Tarjan marks the scc number naturally forms reverse topological order
            if (u == v) break;
        }
    }
}

int main() {
    std::ios_base::sync_with_stdio(false);
    std::cin.tie(NULL);

    int n, m;
    if (!(std::cin >> n >> m)) return 0;

    for (int k = 0; k < m; ++k) {
        int i, a, j, b;
        // Input format: variable i takes value a(0/1) or variable j takes value b(0/1)
        std::cin >> i >> a >> j >> b;

        // State mapping: a == 0 represents false(i+n), a == 1 represents true(i)
        int u_true = i, u_false = i + n;
        int v_true = j, v_false = j + n;

        // Determine the actual state based on 0/1 input
        int pos_u = (a == 1) ? u_true : u_false;
        int neg_u = (a == 1) ? u_false : u_true;
        int pos_v = (b == 1) ? v_true : v_false;
        int neg_v = (b == 1) ? v_false : v_true;

        // Core condition transformation: pos_u V pos_v  <=>  (neg_u -> pos_v) AND (neg_v -> pos_u)
        adj[neg_u].push_back(pos_v);
        adj[neg_v].push_back(pos_u);
    }

    // 1. Run Tarjan to partition the strongly connected topological space
    for (int i = 1; i <= 2 * n; ++i) {
        if (!dfn[i]) {
            tarjan(i);
        }
    }

    // 2. Completeness compliance check
    for (int i = 1; i <= n; ++i) {
        if (scc[i] == scc[i + n]) {
            std::cout << "IMPOSSIBLE\n"; // Positive and negative states belong to the same SCC, logic collapse
            return 0;
        }
    }

    std::cout << "POSSIBLE\n";
    // 3. Use the reverse topological property of the strongly connected component numbers to construct a greedy consistent solution
    for (int i = 1; i <= n; ++i) {
        // The smaller the scc number, the closer it is to the topological order.
        // If scc[i] < scc[i+n], it means the positive state i is behind, so choose the positive state (assign as 1)
        if (scc[i] < scc[i + n]) {
            std::cout << 1 << (i == n ? "" : " ");
        } else {
            std::cout << 0 << (i == n ? "" : " ");
        }
    }
    std::cout << "\n";

    return 0;
}

NOIP 实战避坑指南

强连通编号与拓扑序方向记反：这是2-SAT输出方案时最高频的爆零点。Tarjan算法生成的 scc 缩点编号，在本质上是“逆拓扑序”（即最先被切断弹出的叶子子树其 scc 编号为1）。因此，scc[i] < scc[i+n] 意味着节点 $i$ 在有向图拓扑网络中处于更加靠后的位置。为了避免逻辑污染，我们要选靠后的点，所以此时应该选 $i$，即方案输出 1。如果选手误记为“编号小的拓扑靠前”，将输出逻辑反置，就会导致满盘皆输。
数组空间未开 2 倍（或 4 倍）： 2-SAT伴随着变量拆点，点的总数直接翻倍变为 $2N$。而由于每个析取约束会对应两条蕴含边，边的总数也会翻倍变为 $2M$。选手的 adj 邻接表基座、Tarjan相关的 dfn、low、scc 数组必须雷打不动地开辟2倍（点数）和4倍（边数）空间，否则在建边和递归松弛时会引发严重的越界。

经典 NOIP/洛谷真题

1. 洛谷 P4782 【模板】2-SAT 问题

题意描述：给出一个由 $N$ 个布尔变量和 $M$ 个条件组成的2-SAT问题，每个条件形式为 “$x_i$ 为真/假或 $x_j$ 为真/假”。判断是否有解，若有解则输出一组合法赋值。
问题本质与核心思路：最纯粹的2-SAT模板真题。核心策略完全同构于上述的标准工业源码：首先将每个变量指派为正反两个虚空节点，读入条件后按照蕴含式代数规则进行双向有向边组装；跑Tarjan检查是否存在 scc[i] == scc[i+n]。若安全，则直接利用 scc 逆拓扑序的小根贪心策略直接拉平打印出一组合法解。

2. 洛谷 P3201 [HNOI2009] 梦幻布丁

题意描述：有 $N$ 个排成一排的布丁，每个布丁都有一个初始颜色。现在有 $M$ 次操作，操作分为两种：1. 将颜色 $x$ 的布丁全部变成颜色 $y$。2. 询问当前整条序列上有多少个颜色段（相邻且颜色相同的布丁算作一段）。
问题本质与核心思路：这道题目虽然在官网上属于经典的“线段树合并 / 链表启发式合并”范畴，但它在状态关联和颜色依赖关系的维护上，与2-SAT的“拆点蕴含同构”有着极其微妙的拓扑等价性。在处理颜色修改时，如果直接暴力修改会导致复杂度退化。我们可以使用映射法（指针拓扑化）：不真正去修改底层的颜色，而是维护一个“名义颜色到实际颜色”的映射指针。当要把颜色 $x$ 改成 $y$ 时，实际上是在有向逻辑中将指向 $x$ 的连接直接归拢到 $y$ 上。这种通过修改关系的代理人来平拉时间复杂度的战术，与2-SAT放弃直接搜索真值转而通过有向图蕴含边来框定变量范围的升维思想如出一辙。

In-Depth Analysis of 2-SAT Problem: Efficient Solutions Based on Topological Sorting and Strongly Connected Components