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:
(x0 OR x1) AND (~x0 OR x2) AND (~x1 OR ~x2)
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.
- Create the inference graph G such that for each variable xi in the 2-SAT instance, xi and ~xi are vertices of the inference graph. xi and ~xi are complements of each other.
- For each clause (u OR v), add the edges ~u -> v and ~v -> u to the inference graph G.
- 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.
- 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.