In computer science, 2-satisfiability (abbreviated as 2-SAT) is the problem of determining whether a collection of two-valued (Boolean or binary) variables with constraints on pairs of variables can be assigned values satisfying all the constraints. In contrast with 3-satisfiability and with constraint satisfaction problems with more than two values per variable, it may be solved in polynomial time.

Applications

A number of exact and approximate algorithms for the automatic label placement problem are based on 2-satisfiability. This problem concerns placing textual labels on the features of a diagram or map. Typically, these labels are highly constrained, not only by the map itself (they must be near the feature they label, and not obscure other features), but by each other: two labels will be illegible if they overlap each other. In general, label placement is an NP-hard problem. However, if each feature has only two possible locations for its label (say, extending to the left and to the right of the feature) then it may be solved in polynomial time. For, in this case, one may create a 2-satisfiability instance that has a variable for each label and constraints preventing each pair of labels from being assigned overlapping positions. Similar reductions to 2-satisfiability have been applied to other geometric placement problems including reflection of modules in VLSI designs and edge routing in graph drawing and VLSI layout.

2-satisfiability has also been applied to problems of clustering a set of data points into two clusters minimizing the sum of the cluster diameters, choosing which games in a round-robin tournament schedule to play as home games or away games, recognizing undirected graphs that can be partitioned into an independent set and a small number of complete bipartite subgraphs, inferring business relationships among autonomous subsystems of the internet, reconstruction of evolutionary trees, and digital tomography (reconstructing shapes from cross-sections, as in Nonogram puzzles).

Conjunctive normal form and implicative normal form

2-SAT instances are normally presented in conjunctive normal form with two variables per clause (2-CNF). That is, the problem is represented as an expression that is a conjunction of disjunctions, where each disjunction has two arguments that may either be variables or the negations of variables. For example, the following formula is in conjunctive normal form, with seven variables and eleven clauses:

$scriptstyle(x\_0lor\; x\_2)land(x\_0lorlnot\; x\_3)land(x\_1lorlnot\; x\_3)land(x\_1lorlnot\; x\_4)land(x\_2lorlnot\; x\_4)land\{\}atopscriptstylequad\; (x\_0lor\; x\_5)land\; (x\_1lor\; x\_5)land\; (x\_2lor\; x\_5)land\; (x\_3lor\; x\_6)land\; (x\_4lor\; x\_6)land\; (x\_5lor\; x\_6).$

As shown above, each variable may occur in multiple clauses of the expression. The 2-satisfiability problem is to find a truth assignment to these variables that makes a formula of this type true. For the expression shown above, one possible satisfying assignment is the one that sets all the variables to true; there are 15 other satisfying assignments as well. Thus, the instance represented by this expression is satisfiable.

The disjunction of any pair of variables is logically equivalent to an implication, in either of two directions:

$scriptstyle(x\_0lorlnot\; x\_3)\; equiv\; (lnot\; x\_0Rightarrowlnot\; x\_3)\; equiv\; (x\_3Rightarrow\; x\_0).$

Therefore, a 2-satisfiability instance may also be written in implicative normal form, in which we replace each disjunction by the two implications to which it is equivalent. The implicative normal form of a 2-satisfiability problem can be represented as an implication graph, a skew-symmetric directed graph in which there is one vertex per variable or negated variable, and an edge connecting one vertex to another whenever the corresponding variables are related by an implication in the implicative normal form of the instance.

Solution procedures

Unlike general satisfiability or 3-satisfiability which are NP-complete and have no known efficient algorithm, 2-satisfiability can be solved in polynomial time. As observed, a 2-satisfiability instance is solvable if and only if there is no strongly connected component of the implication graph that contains both some variable and its negation. Since strongly connected components may be found in linear time by an algorithm based on depth first search, the same linear time bound applies as well to 2-satisfiability.

It is also possible to solve 2-satisfiability instances in polynomial time using first-order resolution. Each instance of the resolution rule amounts to finding two implications $aRightarrow\; b$ and $bRightarrow\; c$, and inferring by transitivity a third implication $aRightarrow\; c$. Thus, if one applies this rule until no more implications can be inferred, the resulting collection of implications is described by the transitive closure of the implication graph, which has polynomial size. The instance is satisfiable if and only if resolution cannot derive an empty clause in the conjunctive normal form of the instance. However, this procedure, while taking only polynomial time, is not as efficient as the linear-time strongly connected component analysis of Aspvall et al.

Computational complexity

2-satisfiability is NL-complete, meaning that it is one of the "hardest" or "most expressive" problems which can be solved by a nondeterministic Turing machine using only a logarithmic amount of writable memory. The class of problems that can be solved within these space bounds is called NL.

A nondeterministic logspace algorithm for determining whether a 2-satisfiability instance is not satisfiable is easy to describe: simply choose (nondeterministically) a variable v and search (nondeterministically) for a chain of implications leading from v to its negation and then back to v. If such a chain is found, the instance cannot be satisfiable. By the Immerman-Szelepcsényi theorem, it is also possible in nondeterministic logspace to verify that a satisfiable 2-SAT instance is satisfiable.

The set of all solutions

The set of all solutions to a 2-satisfiability instance has the structure of a median graph, in which an edge corresponds to the operation of flipping the values of a set of variables that are all constrained to be equal or unequal to each other. In particular, by following edges in this way one can get from any solution to any other solution. Conversely, any median graph can be represented as the set of solutions to a 2-satisfiability instance in this way. The median of any three solutions is formed by setting each variable to the value it holds in the majority of the three solutions; this median always forms another solution to the instance. describes an algorithm for efficiently listing all solutions to a given 2-satisfiability instance, and for solving several related problems. Algorithms are also known for counting the number of solutions, more quickly than it would be possible to list all solutions, and for finding pairs of solutions that differ as greatly as possible.

Random 2-satisfiability instances

One can form a 2-satisfiability instance at random, for a given number n of variables and m of clauses, by choosing each clause uniformly at random from the set of all possible two-variable clauses. When m is small relative to n, such an instance will likely be satisfiable, but larger values of m have smaller probabilities of being satisfiable. More precisely, if m/n is fixed as a constant α ≠ 1, the probability of satisfiability tends to a limit as n goes to infinity: if α < 1, the limit is one, while if α > 1, the limit is zero. Thus, the problem exhibits a phase transition at α = 1.

Maximum-2-satisfiability

A related problem is maximum-2-satisfiability (MAX-2-SAT) in which the input is still a conjunctive normal form expression with two variables or negated variables per clause but in which the task is to determine the maximum number of clauses that can be simultaneously satisfied by an assignment. MAX-2-SAT is NP-Hard. It is a particular case of maximum-satisfiability.

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.931 times the optimal number of clauses. If P ≠ NP, it is impossible to approximate MAX 2-SAT to within an approximation ratio better than 21/22 in polynomial time.

Various authors have also explored exponential worst-case time bounds for exact solution of MAX-S-SAT instances.

References