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

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 Practical Pitfall Guide

Confusing Strongly Connected Component Numbers with Topological Order Directions: This is the most frequent failure point when outputting solutions for 2-SAT. The scc component numbers generated by Tarjan's algorithm are essentially in "reverse topological order" (i.e., the leaf subtree that gets cut off first has an scc number of 1). Therefore, scc[i] < scc[i+n] means that node $i$ is positioned further back in the directed graph's topological network. To avoid logical contamination, we should select the later node, hence we should choose $i$, which means the solution outputs 1. If contestants mistakenly remember that "smaller numbered topological nodes are ahead", it will invert the logic and lead to a complete loss.
Not Allocating 2x (or 4x) Array Space: 2-SAT involves splitting variables, which directly doubles the total number of nodes to $2N$. Since each disjunctive constraint corresponds to two implication edges, the total number of edges also doubles to $2M$. Contestants must unwaveringly allocate 2x (for nodes) and 4x (for edges) space for the adj adjacency list base, as well as Tarjan-related dfn, low, and scc arrays; otherwise, serious out-of-bounds issues will arise during edge construction and recursive relaxation.

Classic NOIP/Luogu Real Questions

1. Luogu P4782 [Template] 2-SAT Problem

Problem Description: Given a 2-SAT problem composed of $N$ Boolean variables and $M$ conditions, each condition is in the form of "$x_i$ is true/false or $x_j$ is true/false". Determine if there is a solution, and if so, output a valid assignment.
Core Idea and Key Approach: This is the purest 2-SAT template problem. The core strategy is completely isomorphic to the standard industrial source code mentioned above: first assign each variable to two virtual nodes (positive and negative), read in the conditions, and assemble bidirectional directed edges according to implication algebra rules; run Tarjan to check for scc[i] == scc[i+n]. If safe, directly use the greedy strategy based on the small root of the scc reverse topological order to flatten and print a valid solution.

2. Luogu P3201 [HNOI2009] Dream Pudding

Problem Description: There are $N$ puddings lined up, each with an initial color. Now there are $M$ operations, which are of two types: 1. Change all puddings of color $x$ to color $y$. 2. Ask how many color segments there are in the current sequence (adjacent puddings of the same color count as one segment).
Core Idea and Key Approach: Although this question belongs to the classic "segment tree merging / heuristic merging of linked lists" category on the official website, it has a remarkably subtle topological equivalence with the 2-SAT's "splitting points and implications" in terms of state association and color dependency maintenance. When handling color modifications, directly modifying the underlying color would cause a degradation in complexity. We can use mapping method (pointer topologization): instead of actually modifying the underlying colors, maintain a mapping pointer from "nominal color to actual color". When changing color $x$ to $y$, we essentially redirect the connections pointing to $x$ directly to $y$. This tactic of modifying the relationship agent to flatten the time complexity is reminiscent of the 2-SAT's approach of bounding variable ranges through directed graph implication edges rather than direct truth value search.