Satisfiability
An instance of the 2-satisfiability problem, that is, a Boolean expression in conjunctive normal form with two variables or negations of variables per clause, may be transformed into an implication graph by replacing each clause by the two implications and . This graph has a vertex for each variable or negated variable, and a directed edge for each implication; it is, by construction, skew-symmetric, with a correspondence σ that maps each variable to its negation. As Aspvall, Plass & Tarjan (1979) showed, a satisfying assignment to the 2-satisfiability instance is equivalent to a partition of this implication graph into two subsets of vertices, S and σ(S), such that no edge starts in S and ends in σ(S). If such a partition exists, a satisfying assignment may be formed by assigning a true value to every variable in S and a false value to every variable in σ(S). This may be done if and only if no strongly connected component of the graph contains both some vertex v and its complementary vertex σ(v). If two vertices belong to the same strongly connected component, the corresponding variables or negated variables are constrained to equal each other in any satisfying assignment of the 2-satisfiability instance. The total time for testing strong connectivity and finding a partition of the implication graph is linear in the size of the given 2-CNF expression.
Read more about this topic: Skew-symmetric Graph