Complexity Analysis

Building the graph takes $O(C)$ time where C is the number of clauses. Each clause adds exactly two edges to the graph. SCC computation is $O(V + E)$ for both Kosaraju and Tarjan. Here V = $2n$ (n variables, each has two nodes) and E = $2C$ (each clause makes two edges).

Checking satisfiability and constructing the assignment both take $O(n)$ time. Total: $O(n + C)$, which is linear in the input size. That is why $2$-SAT is tractable while general SAT is not. The restriction to two literals per clause makes all the difference.

Space complexity is $O(V)$ for the data structures used.