2-satisfiability

Both of these kinds of inputs may be solved in linear time, either by a method based on backtracking or by using the strongly connected components of the implication graph.

A computationally difficult variation of 2-satisfiability, finding a truth assignment that maximizes the number of satisfied constraints, has an approximation algorithm whose optimality depends on the unique games conjecture, and another difficult variation, finding a satisfying assignment minimizing the number of true variables, is an important test case for parameterized complexity.

Because finding a satisfying assignment using Krom's method involves a sequence of O(n) consistency checks, it would take time O(n4).

Even, Itai & Shamir (1976) quote a faster time bound of O(n2) for this algorithm, based on more careful ordering of its operations.

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.

[5] Aspvall, Plass & Tarjan (1979) found a simpler linear time procedure for solving 2-satisfiability instances, based on the notion of strongly connected components from graph theory.

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.

[4] 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.

They observe that this version of the problem may be solved as a 2-satisfiability instance, in which the constraints relate the orientations of pairs of modules that are directly across the channel from each other.

As a consequence, the optimal density may also be calculated efficiently, by performing a binary search in which each step involves the solution of a 2-satisfiability instance.

To find the optimal sum of diameters one may perform a binary search in which each step is a feasibility test of this type.

[5] Miyashiro & Matsui (2005) apply 2-satisfiability to a problem of sports scheduling, in which the pairings of a round-robin tournament have already been chosen and the games must be assigned to the teams' stadiums.

For instance, in the popular nonogram puzzles, also known as paint by numbers or griddlers, the set of squares to be determined represents the dark pixels in a binary image, and the input given to the puzzle solver tells him or her how many consecutive blocks of dark pixels to include in each row or column of the image, and how long each of those blocks should be.

[21] An even more constrained version that is easier to solve is that the shape is orthogonally convex: having a single contiguous block of squares in each row and column.

Improving several previous solutions, Chrobak & Dürr (1999) showed how to reconstruct connected orthogonally convex shapes efficiently, using 2-SAT.

[23] A part of a solver for full nonogram puzzles, Batenburg and Kosters (2008, 2009) used 2-satisfiability to combine information obtained from several other heuristics.

They also transform the nonogram into a digital tomography problem by replacing the sequence of block lengths in each row and column by its sum, and use a maximum flow formulation to determine whether this digital tomography problem combining all of the rows and columns has any squares whose state can be determined or pairs of squares that can be connected by an implication relation.

Batenburg and Kosters report that, although most newspaper puzzles do not need its full power, both this procedure and a more powerful but slower procedure which combines this 2-satisfiability approach with the limited backtracking of Even, Itai & Shamir (1976)[5] are significantly more effective than the dynamic programming and flow heuristics without 2-satisfiability when applied to more difficult randomly generated nonograms.

Lewis (1978) found a generalization of this class, renamable Horn satisfiability, that can still be solved in polynomial time by means of an auxiliary 2-satisfiability instance.

[26] 2-satisfiability has also been applied to problems of recognizing undirected graphs that can be partitioned into an independent set and a small number of complete bipartite subgraphs,[27] inferring business relationships among autonomous subsystems of the internet,[28] and reconstruction of evolutionary trees.

Analogously to similar results for the more well-known complexity class NP, this transformation together with the Immerman–Szelepcsényi theorem allow any problem in NL to be represented as a second order logic formula with a single existentially quantified predicate with clauses limited to length 2.

[31] Similarly, the implicative normal form can be expressed in first order logic with the addition of an operator for transitive closure.

[36] The fastest known algorithm for computing the exact number of satisfying assignments to a 2SAT formula runs in time

[41] By formulating MAX-2-SAT as a problem of finding a cut (that is, a partition of the vertices into two subsets) maximizing the number of edges that have one endpoint in the first subset and one endpoint in the second, in a graph related to the implication graph, and applying semidefinite programming methods to this cut problem, it is possible to find in polynomial time an approximate solution that satisfies at least 0.940... times the optimal number of clauses.

[44] Under the weaker assumption that P ≠ NP, the problem is only known to be inapproximable within a constant better than 21/22 = 0.95454...[45] Various authors have also explored exponential worst-case time bounds for exact solution of MAX-2-SAT instances.

-variable 2SAT instance and an integer k, and the problem is to decide whether there exists a satisfying assignment in which exactly k of the variables are true.

Each edge uv of the graph may be represented by a 2SAT clause u ∨ v that can be satisfied only by including either u or v among the true variables of the solution.

Aspvall, Plass & Tarjan (1979) showed that it can be solved in linear time, by an extension of their technique of strongly connected components and topological ordering.