Editing 2-satisfiability (section)

===Strongly connected components===
{{harvtxt|Aspvall|Plass|Tarjan|1979}} found a simpler linear time procedure for solving 2-satisfiability instances, based on the notion of [[strongly connected component]]s from [[graph theory]].<ref name="APT79"/>

Two vertices in a directed graph are said to be strongly connected to each other if there is a directed path from one to the other and vice versa. This is an [[equivalence relation]], and the vertices of the graph may be partitioned into strongly connected components, subsets within which every two vertices are strongly connected. There are several efficient linear time algorithms for finding the strongly connected components of a graph, based on [[depth-first search]]: [[Tarjan's strongly connected components algorithm]]<ref>{{citation|first=Robert E.|last=Tarjan|author-link=Robert Tarjan|title=Depth-first search and linear graph algorithms|journal=[[SIAM Journal on Computing]]|volume=1|year=1972|issue=2|pages=146–160|doi=10.1137/0201010|s2cid=16467262 }}.</ref> and the [[path-based strong component algorithm]]<ref>First published by {{citation
 | last1 = Cheriyan | first1 = J.
 | last2 = Mehlhorn | first2 = K. | author2-link = Kurt Mehlhorn
 | doi = 10.1007/BF01940880
 | journal = [[Algorithmica]]
 | pages = 521–549
 | title = Algorithms for dense graphs and networks on the random access computer
 | volume = 15
 | year = 1996
 | issue = 6| s2cid = 8930091
 }}. Rediscovered in 1999 by [[Harold N. Gabow]], and published in {{citation
 | last = Gabow | first = Harold N.| contribution = Searching (Ch 10.1)
 | editor1-last = Gross | editor1-first = J. L.
 | editor2-last = Yellen | editor2-first = J.
 | pages = 953–984
 | publisher = CRC Press
 | title = Discrete Math. and its Applications: Handbook of Graph Theory
 | volume = 25
 | year = 2003}}.</ref> each perform a single depth-first search. [[Kosaraju's algorithm]] performs two depth-first searches, but is very simple.

In terms of the implication graph, two literals belong to the same strongly connected component whenever there exist chains of implications from one literal to the other and vice versa. Therefore, the two literals must have the same value in any satisfying assignment to the given 2-satisfiability instance. In particular, if a variable and its negation both belong to the same strongly connected component, the instance cannot be satisfied, because it is impossible to assign both of these literals the same value. As Aspvall et al. showed, this is a [[necessary and sufficient condition]]: a 2-CNF formula is satisfiable if and only if there is no variable that belongs to the same strongly connected component as its negation.<ref name="APT79"/>

This immediately leads to a linear time algorithm for testing satisfiability of 2-CNF formulae: simply perform a strong connectivity analysis on the implication graph and check that each variable and its negation belong to different components. However, as Aspvall et al. also showed, it also leads to a linear time algorithm for finding a satisfying assignment, when one exists. Their algorithm performs the following steps:
*Construct the implication graph of the instance, and find its strongly connected components using any of the known linear-time algorithms for strong connectivity analysis.
*Check whether any strongly connected component contains both a variable and its negation. If so, report that the instance is not satisfiable and halt.
*Construct the [[Strongly connected component|condensation]] of the implication graph, a smaller graph that has one vertex for each strongly connected component, and an edge from component {{math|''i''}} to component {{math|''j''}} whenever the implication graph contains an edge {{math|''uv''}} such that {{math|''u''}} belongs to component {{math|''i''}} and {{math|''v''}} belongs to component {{math|''j''}}. The condensation is automatically a [[directed acyclic graph]] and, like the implication graph from which it was formed, it is [[Skew-symmetric graph|skew-symmetric]].
*[[Topological sorting|Topologically order]] the vertices of the condensation.  In practice this may be efficiently achieved as a side effect of the previous step, as components are generated by Kosaraju's algorithm in topological order and by Tarjan's algorithm in reverse topological order.<ref>{{citation|last=Harrison|first=Paul|title=Robust topological sorting and Tarjan's algorithm in Python|url=http://www.logarithmic.net/pfh/blog/01208083168|access-date=9 February 2011}}</ref>
*For each component in the reverse topological order, if its variables do not already have truth assignments, set all the literals in the component to be true. This also causes all of the literals in the complementary component to be set to false.

Due to the reverse topological ordering and the skew-symmetry, when a literal is set to true, all literals that can be reached from it via a chain of implications will already have been set to true. Symmetrically, when a literal {{math|''x''}} is set to false, all literals that lead to it via a chain of implications will themselves already have been set to false. Therefore, the truth assignment constructed by this procedure satisfies the given formula, which also completes the proof of correctness of the necessary and sufficient condition identified by Aspvall et al.<ref name="APT79"/>

As Aspvall et al. show, a similar procedure involving topologically ordering the strongly connected components of the implication graph may also be used to evaluate [[True quantified Boolean formula|fully quantified Boolean formulae]] in which the formula being quantified is a 2-CNF formula.<ref name="APT79"/>