page_title: Skew-symmetric graph
section_title: Satisfiability
hierarchical_section_title: Skew-symmetric graph / Satisfiability
context_page_description: In graph theory, a branch of mathematics, a skew-symmetric graph is a directed graph that is isomorphic to its own transpose graph, the graph formed by reversing all of its edges, under an isomorphism that is an involution without any fixed points. Skew-symmetric graphs are identical to the double covering graphs of bidirected graphs.
  Skew-symmetric graphs were first introduced under the name of antisymmetrical digraphs by Tutte, later as the double covering graphs of polar graphs by Zelinka, and still later as the double covering graphs of bidirected graphs by Zaslavsky. They arise in modeling the search for alternating paths and alternating cycles in algorithms for finding matchings in graphs, in testing whether a still life pattern in Conway's Game of Life may be partitioned into simpler components, in graph drawing, and in the implication graphs used to efficiently solve the 2-satisfiability problem.
context_section_description: 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.
caption: An implication graph. Its skew symmetry can be realized by rotating the graph through a 180 degree angle and reversing all edges.