Editing 2-satisfiability (section)

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