Solving 2-SAT in linear time

2-Satisfiability (2-SAT) is the problem of determining whether a collection of boolean variables with constraints on pairs of variables can be assigned values satisfying all the constraints. Although 3-SAT is NP complete, 2-SAT can be solved in linear time.

A 2-SAT instance can be described using 2-CNF as follows:
(x₀ OR x₁) AND (~x₀ OR x₂) AND (~x₁ OR ~x₂)
The 2-SAT problem is to find a truth assignment to these variables that makes a formula of this type true: we must choose whether to make each of the variables true or false, so that every clause has at least one term that becomes true.
Aspvall, Plass & Tarjan (1979) found a simple linear time procedure for solving 2-SAT instances, based on the notion of strongly connected components. The algorithm is as follows:

1. Create the inference graph G such that for each variable x_i in the 2-SAT instance, x_i and ~x_i are vertices of the inference graph. x_i and ~x_i are complements of each other.
2. For each clause (u OR v), add the edges ~u -> v and ~v -> u to the inference graph G.
3. Process the strongly connected components S of G in reverse topological order as follows: If S is marked, do nothing. If S = ~S (i.e., a variable and its complement belong to the same SCC), then stop, the instance is unsatisfiable. Otherwise, mark S true and ~S false.
4. We get a satisfying assignment by assigning to each variable the truth value of the component containing it.

Take a look at the C++ implementation.