Editing 2-satisfiability (section)

==Algorithms==
Several algorithms are known for solving the 2-satisfiability problem. The most efficient of them take [[linear time]].<ref name="Krom1967"/><ref name="APT79"/><ref name="EIS76"/>

===Resolution and transitive closure===
{{harvtxt|Krom|1967}} described the following [[polynomial time]] decision procedure for solving 2-satisfiability instances.<ref name="Krom1967"/>

Suppose that a 2-satisfiability instance contains two clauses that both use the same variable ''x'', but that ''x'' is negated in one clause and not in the other. Then the two clauses may be combined to produce a third clause, having the two other literals in the two clauses; this third clause must also be satisfied whenever the first two clauses are both satisfied. This is called  [[resolution (logic)|resolution]]. For instance, we may combine the clauses <math>(a\lor b)</math> and <math>(\lnot b\lor\lnot c)</math> in this way to produce the clause <math>(a\lor\lnot c)</math>. In terms of the implicative form of a 2-CNF formula, this rule amounts to finding two implications <math>\lnot a\Rightarrow b</math> and <math>b\Rightarrow \lnot c</math>, and inferring by [[transitive relation|transitivity]] a third implication <math>\lnot a\Rightarrow \lnot c</math>.<ref name="Krom1967"/>

Krom writes that a formula is ''consistent'' if repeated application of this inference rule cannot generate both the clauses <math>(x\lor x)</math> and <math> (\lnot x\lor\lnot x)</math>, for any variable <math> x</math>. As he proves, a 2-CNF formula is satisfiable if and only if it is consistent. For, if a formula is not consistent, it is not possible to satisfy both of the two clauses <math> (x\lor x)</math> and <math>(\lnot x\lor\lnot x)</math> simultaneously. And, if it is consistent, then the formula can be extended by repeatedly adding one clause of the form <math> (x\lor x)</math> or <math> (\lnot x\lor\lnot x)</math> at a time, preserving consistency at each step, until it includes such a clause for every variable. At each of these extension steps, one of these two clauses may always be added while preserving consistency, for if not then the other clause could be generated using the inference rule. Once all variables have a clause of this form in the formula, a satisfying assignment of all of the variables may be generated by setting a variable <math> x</math> to true if the formula contains the clause <math> (x\lor x)</math> and setting it to false if the formula contains the clause <math>(\lnot x\lor\lnot x)</math>.<ref name="Krom1967"/>

Krom was concerned primarily with [[completeness (logic)|completeness]] of systems of inference rules, rather than with the efficiency of algorithms. However, his method leads to a [[polynomial time]] bound for solving 2-satisfiability problems. By grouping together all of the clauses that use the same variable, and applying the inference rule to each pair of clauses, it is possible to find all inferences that are possible from a given 2-CNF instance, and to test whether it is consistent, in total time {{math|O(''n''<sup>3</sup>)}}, where {{math|''n''}} is the number of variables in the instance. This formula comes from multiplying the number of variables by the {{math|O(''n''<sup>2</sup>)}} number of pairs of clauses involving a given variable, to which the inference rule may be applied. Thus, it is possible to determine whether a given 2-CNF instance is satisfiable in time {{math|O(''n''<sup>3</sup>)}}. Because finding a satisfying assignment using Krom's method involves a sequence of {{math|O(''n'')}} consistency checks, it would take time {{math|O(''n''<sup>4</sup>)}}. {{harvtxt|Even|Itai|Shamir|1976}} quote a faster time bound of {{math|O(''n''<sup>2</sup>)}} for this algorithm, based on more careful ordering of its operations. Nevertheless, even this smaller time bound was greatly improved by the later linear time algorithms of {{harvtxt|Even|Itai|Shamir|1976}} and {{harvtxt|Aspvall|Plass|Tarjan|1979}}.

In terms of the implication graph of the 2-satisfiability instance, Krom's inference rule can be interpreted as constructing the [[transitive closure]] of the graph. As {{harvtxt|Cook|1971}} observes, it can also be seen as an instance of the [[Davis–Putnam algorithm]] for solving satisfiability problems using the principle of [[Resolution (logic)|resolution]]. Its correctness follows from the more general correctness of the Davis–Putnam algorithm. Its polynomial time bound follows from the fact that each resolution step increases the number of clauses in the instance, which is upper bounded by a quadratic function of the number of variables.<ref>{{citation|first=Stephen A.|last=Cook|author-link=Stephen Cook|contribution=The complexity of theorem-proving procedures|title=Proc. 3rd ACM Symp. Theory of Computing (STOC)|year=1971|pages=151–158|doi=10.1145/800157.805047|s2cid=7573663|doi-access=free}}.</ref>

===Limited backtracking===
{{harvtxt|Even|Itai|Shamir|1976}} describe a technique involving limited [[backtracking]] for solving constraint satisfaction problems with [[binary data|binary variables]] and pairwise constraints. They apply this technique to a problem of classroom scheduling, but they also observe that it applies to other problems including 2-SAT.<ref name="EIS76">{{citation|first1=S.|last1=Even|author1-link=Shimon Even|first2=A.|last2=Itai|first3=A.|last3=Shamir|author3-link=Adi Shamir|title=On the complexity of time table and multi-commodity flow problems|journal=[[SIAM Journal on Computing]]|volume=5|issue=4|year=1976|pages=691–703|doi=10.1137/0205048}}.</ref>

The basic idea of their approach is to build a partial truth assignment, one variable at a time. Certain steps of the algorithms are "choice points", points at which a variable can be given either of two different truth values, and later steps in the algorithm may cause it to backtrack to one of these choice points. However, only the most recent choice can be backtracked over. All choices made earlier than the most recent one are permanent.<ref name="EIS76"/>

Initially, there is no choice point, and all variables are unassigned. At each step, the algorithm chooses the variable whose value to set, as follows:
*If there is a clause both of whose variables are already set, in a way that falsifies the clause, then the algorithm backtracks to its most recent choice point, undoing the assignments it made since that choice, and reverses the decision made at that choice. If there is no choice point, or if the algorithm has already backtracked over the most recent choice point, then it aborts the search and reports that the input 2-CNF formula is unsatisfiable.
*If there is a clause in which one of the clause's two variables has already been set, and the clause could still become either true or false, then the other variable is set in a way that forces the clause to become true.
*In the remaining case, each clause is either guaranteed to become true no matter how the remaining variables are assigned, or neither of its two variables has been assigned yet. In this case the algorithm creates a new choice point and sets any one of the unassigned variables to an arbitrarily chosen value.

Intuitively, the algorithm follows all chains of inference after making each of its choices. This either leads to a contradiction and a backtracking step, or, if no contradiction is derived, it follows that the choice was a correct one that leads to a satisfying assignment. Therefore, the algorithm either correctly finds a satisfying assignment or it correctly determines that the input is unsatisfiable.<ref name="EIS76"/>

Even et al. did not describe in detail how to implement this algorithm efficiently. They state only that by "using appropriate data structures in order to find the implications of any decision", each step of the algorithm (other than the backtracking) can be performed quickly. However, some inputs may cause the algorithm to backtrack many times, each time performing many steps before backtracking, so its overall complexity may be nonlinear. To avoid this problem, they modify the algorithm so that, after reaching each choice point, it begins simultaneously testing both of the two assignments for the variable set at the choice point, spending equal numbers of steps on each of the two assignments. As soon as the test for one of these two assignments would create another choice point, the other test is stopped, so that at any stage of the algorithm there are only two branches of the backtracking tree that are still being tested. In this way, the total time spent performing the two tests for any variable is proportional to the number of variables and clauses of the input formula whose values are permanently assigned. As a result, the algorithm takes [[linear time]] in total.<ref name="EIS76"/>

===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"/>