2-satisfiability

In computer science, 2-satisfiability (abbreviated as 2-SAT or just 2SAT) 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 has a known polynomial time solution. Instances of the 2-satisfiability problem are known as 2-CNF formulas or Krom formulas.

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

The implication graph for the example 2-SAT instance shown in this section.

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_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \scriptstyle \quad (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor 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_{0}\lor \lnot x_{3})\equiv (\lnot x_{0}\Rightarrow \lnot x_{3})\equiv (x_{3}\Rightarrow x_{0}).$

Therefore, a 2-satisfiability instance may also be written in implicative normal form, in which we replace each disjunction by one of 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.

Algorithms

Unlike 3-satisfiability which is NP-complete and has no known efficient algorithm, 2-satisfiability can be solved in polynomial time. As Krom (1967) observed, a 2-satisfiability instance is satisfiable if and only if every variable of the instance belongs to a different strongly connected component of the implication graph than the negation of the same variable. Consequently, 2-SAT instances are commonly referred to as Krom formulas. This was later rediscovered by Aspvall, Plass & Tarjan (1979). 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, per Cook (1971). Each instance of the resolution rule amounts to finding two implications $a\Rightarrow b$ and $b\Rightarrow c$, and inferring by transitivity a third implication $a\Rightarrow 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.

Complexity and extensions

NL-completeness

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. These problems can be characterized by second order logic formulas in 2-CNF form; the set of formulas defined in this way is denoted SO(Krom).

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 median graph representing all solutions to the example 2-SAT instance shown above.

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.

Feder (1994) describes an algorithm for efficiently listing all solutions to a given 2-satisfiability instance, and for solving several related problems. There also exist algorithms for finding two satisfying assignments that have the maximal Hamming distance from each other.

Counting the number of satisfying assignments

#2SAT is the problem of counting the number of satisfying assignments to a given 2-CNF formula. This counting problem is #P-complete, which implies that it is not solvable in polynomial time unless P = NP. Moreover, there is no fully polynomial randomized approximation scheme for #2SAT unless NP = RP and this even holds when the input is restricted to monotone 2-CNF formulas, i.e., 2-CNF formulas in which each literal is a positive occurrence of a variable.

The fastest known algorithm for computing the exact number of satisfying assignments to a 2SAT formula runs in time $O(1.246^{n})$.

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

In the maximum-2-satisfiability problem (MAX-2-SAT), the input is a formula in conjunctive normal form with two literals per clause, and the task is to determine the maximum number of clauses that can be simultaneously satisfied by an assignment. MAX-2-SAT is NP-hard and it is a particular case of a maximum satisfiability problem.

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. A balanced MAX 2-SAT instance is an instance of MAX 2-SAT where every variable appears positively and negatively with equal weight. For this problem, one can improve the approximation ratio to $\min \left\{(3-\cos \theta )^{-1}(2+(2/\pi )\theta )\,:\,\pi /2\leq \theta \leq \pi \right\}=0.943...$.

Assuming the Unique games conjecture, it is impossible to approximate MAX 2-SAT, balanced or not, with an approximation constant better than 0.943... in polynomial time. Under the weaker assumption that P ≠ NP, the problem is only known to be inapproximable within a constant better than 21/22 = 0.95454...

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

Weighted-2-satisfiability

In the weighted 2-satisfiability problem (W2SAT), the input is an $n$-variable 2SAT instance and an integer $k$, and the problem is to decide whether there exists a satisfying assignment of Hamming weight at most $k$. This problem allows to easily encode the Clique problem and is NP-complete. Moreover, it is a natural W[1]-complete problem, which is a notion from parameterized complexity. It implies that W2SAT is not fixed-parameter tractable unless this holds for all problems in W[1], and thus is unlikely to be computable in time $f(k)\cdot n^{O(1)}$. Moreover, W2SAT cannot be computed in time $n^{o(k)}$ unless the exponential time hypothesis fails.