2-satisfiability

From Wikipedia, the free encyclopedia

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.

Contents

[edit] 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.[1] Similar reductions to 2-satisfiability have been applied to other geometric placement problems, including reflection of modules in VLSI designs[2] and edge placement in graph drawing.[3]

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,[4] choosing which games in a round-robin tournament schedule to play as home games or away games,[5] recognizing undirected graphs that can be partitioned into an independent set and a small number of complete bipartite subgraphs,[6] inferring business relationships among autonomous subsystems of the internet,[7] reconstruction of evolutionary trees,[8] and digital tomography (reconstructing shapes from cross-sections, as in Nonogram puzzles).[9]

[edit] Conjunctive normal form and implicative normal form

The implication graph for the example 2-SAT instance shown in this section.
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 x_5)\land (x_1\lor x_5)\land (x_2\lor 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 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.

[edit] 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 Aspvall, Plass & Tarjan (1979) observed,[10] 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.[11] 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 conjuctive 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.

[edit] Computational complexity

2-satisfiability is NL-complete,[12] 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: simple 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.

[edit] The set of all solutions

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

Feder (1994) describes an algorithm for efficiently listing all solutions to a given 2-satisfiability instance, and for solving several related problems.[14] Algorithms are also known for counting the number of solutions, more quickly than it would be possible to list all solutions,[15] and for finding pairs of solutions that differ as greatly as possible.[16]

[edit] 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 zero, while if α > 1, the limit is one. Thus, the problem exhibits a phase transition at α = 1.[17]

[edit] 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.[18] If P ≠ NP, it is impossible to approximate MAX 2-SAT to within an approximation ratio better than 21/22 in polynomial time.[19]

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

[edit] References

  1. ^ Doddi, Srinivas; Marathe, Madhav V.; Mirzaian, Andy; Moret, Bernard M. E. & Zhu, Binhai (1997), “Map labeling and its generalizations”, Proc. 8th ACM-SIAM Symp. Discrete Algorithms (SODA), pp. 148–157, <http://portal.acm.org/citation.cfm?id=314250> ; Formann, M. & Wagner, F. (1991), “A packing problem with applications to lettering of maps”, Proc. 7th ACM Symp. Computational Geometry, pp. 281–288 ; Poon, Chung Keung; Zhu, Binhai & Chin, Francis (1998), “A polynomial time solution for labeling a rectilinear map”, Information Processing Letters 65 (4): 201–207, DOI 10.1016/S0020-0190(98)00002-7 ; Wagner, Frank & Wolff, Alexander (1997), “A practical map labeling algorithm”, Computational Geometry: Theory and Applications 7 (5–6): 387–404, DOI 10.1016/S0925-7721(96)00007-7 .
  2. ^ Boros, Endre; Hammer, Peter L.; Minoux, Michel & Rader, David J., Jr. (1999), “Optimal cell flipping to minimize channel density in VLSI design and pseudo-Boolean optimization”, Discrete Applied Mathematics 90 (1–3): 69–88, DOI 10.1016/S0166-218X(98)00114-0 .
  3. ^ Efrat, Alon; Erten, Cesim & Kobourov, Stephen G. (2007), “Fixed-location circular arc drawing of planar graphs”, Journal of Graph Algorithms and Applications 11 (1): 145–164, <http://jgaa.info/accepted/2007/EfratErtenKobourov2007.11.1.pdf> .
  4. ^ Hansen, P. & Jaumard, B. (1987), “Minimum sum of diameters clustering”, Journal of Classification 4 (2): 215–226, DOI 10.1007/BF01896987 ; Ramnath, Sarnath (2004), “Dynamic digraph connectivity hastens minimum sum-of-diameters clustering”, SIAM Journal on Discrete Mathematics 18 (2): 272–286, DOI 10.1137/S0895480102396099 .
  5. ^ Miyashiro, Ryuhei & Matsui, Tomomi (2005), “A polynomial-time algorithm to find an equitable home–away assignment”, Operations Research Letters 33 (3): 235–241, DOI 10.1016/j.orl.2004.06.004 .
  6. ^ Brandstädt, Andreas; Hammer, Peter L.; Le, Van Bang & Lozin, Vadim V. (2005), “Bisplit graphs”, Discrete Mathematics 299 (1–3): 11–32, DOI 10.1016/j.disc.2004.08.046 .
  7. ^ Wang, Hao; Xie, Haiyong; Yang, Yang Richard; Silberschatz, Avi; Li, Li Erran & Liu, Yanbin (2005), “Stable egress route selection for interdomain traffic engineering: model and analysis”, 13th IEEE Conf. Network Protocols (ICNP), pp. 16–29, DOI 10.1109/ICNP.2005.39 .
  8. ^ Eskin, Eleazar; Halperin, Eran & Karp, Richard M. (2003), “Efficient reconstruction of haplotype structure via perfect phylogeny”, Journal of Bioinformatics and Computational Biology 1 (1): 1–20, <http://www.worldscinet.com/cgi-bin/details.cgi?id=pii:S0219720003000174&type=html> .
  9. ^ Brunetti, Sara & Daurat, Alain (2003), “An algorithm reconstructing convex lattice sets”, Theoretical computer science 304 (1–3): 35–57, DOI 10.1016/S0304-3975(03)00050-1 ; Chrobak, Marek & Dürr, Christoph (1999), “Reconstructing hv-convex polyominoes from orthogonal projections”, Information Processing Letters 69 (6): 283–289, DOI 10.1016/S0020-0190(99)00025-3 ; Kuba, Attila & Balogh, Emese (2002), “Reconstruction of convex 2D discrete sets in polynomial time”, Theoretical Computer Science 283 (1): 223–242, DOI 10.1016/S0304-3975(01)00080-9 .
  10. ^ Aspvall, Bengt; Plass, Michael F. & Tarjan, Robert E. (1979), “A linear-time algorithm for testing the truth of certain quantified boolean formulas”, Information Processing Letters 8 (3): 121–123 .
  11. ^ Cook, Stephen A. (1971), “The complexity of theorem-proving procedures”, Proc. 3rd ACM Symp. Theory of Computing (STOC), pp. 151–158, DOI 10.1145/800157.805047 .
  12. ^ Papadimitriou, Christos H. (1994), Computational Complexity, Addison-Wesley, pp. chapter 4.2, ISBN 0-201-53082-1 ., Thm. 16.3.
  13. ^ Bandelt, Hans-Jürgen & Chepoi, V. (2008), “Metric graph theory and geometry: a survey”, Contemporary Mathematics, <http://www.lif-sud.univ-mrs.fr/%7Echepoi/survey_cm_bis.pdf> , to appear. Chung, F. R. K.; Graham, R. L. & Saks, M. E. (1989), “A dynamic location problem for graphs”, Combinatorica 9: 111–132, <http://www.math.ucsd.edu/~fan/mypaps/fanpap/101location.pdf> . Feder, T. (1995), Stable Networks and Product Graphs, vol. 555, Memoirs of the American Mathematical Society .
  14. ^ Feder, Tomás (1994), “Network flow and 2-satisfiability”, Algorithmica 11 (3): 291–319, DOI 10.1007/BF01240738 .
  15. ^ Dahllöf, Vilhelm; Jonsson, Peter & Wahlström, Magnus (2005), “Counting models for 2SAT and 3SAT formulae”, Theoretical Computer Science 332 (1–3): 265–291, DOI 10.1016/j.tcs.2004.10.037 ; Fürer, Martin & Kasiviswanathan, Shiva Prasad (2007), “Algorithms for counting 2-SAT solutions and colorings with applications”, Algorithmic Aspects in Information and Management, vol. 4508, Lecture Notes in Computer Science, Springer-Verlag, pp. 47–57, DOI 10.1007/978-3-540-72870-2 .
  16. ^ Angelsmark, Ola & Thapper, Johan (2005), “Algorithms for the maximum Hamming distance problem”, Recent Advances in Constraints, vol. 3419, Lecture Notes in Computer Science, Springer-Verlag, pp. 128–141, DOI 10.1007/11402763_10 .
  17. ^ Bollobás, Béla; Borgs, Christian; Chayes, Jennifer T.; Kim, Jeong Han & Wilson, David B. (2001), “The scaling window of the 2-SAT transition”, Random Structures and Algorithms 18 (3): 201–256, DOI 10.1002/rsa.1006 ; Chvátal, V. & Reed, B. (1992), “Mick gets some (the odds are on his side)”, Proc. 33rd IEEE Symp. Foundations of Computer Science (FOCS), pp. 620–627, DOI 10.1109/SFCS.1992.267789 ; Goerdt, A. (1996), “A threshold for unsatisfiability”, Journal of Computer and System Sciences 53: 469–486, DOI 10.1006/jcss.1996.0081 .
  18. ^ Feige, U. & Goemans, M. X. (1995), “Approximating the value of two prover proof systems, with applications to MAX 2SAT and MAX DICUT”, Proc. 3rd Israel Symp. Theory of Computing and Systems, IEEE Computer Society Press, pp. 182–189 . For earlier approximation algorithms with weaker solution quality guarantees, see Goemans, M. X. & Williamson, David P. (1995), “Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming”, Journal of the Association for Computing Machinery 42 (6): 1115–1145, DOI 10.1145/227683.227684  and Yannakakis, Mihalis (1994), “On the approximation of maximum satisfiability”, Journal of Algorithms 17 (3): 475–502, DOI 10.1006/jagm.1994.1045 .
  19. ^ Håstad, Johan (2001), “Some optimal inapproximability results”, Journal of the Association for Computing Machinery 48 (4): 798–859, DOI 10.1145/502090.502098 .
  20. ^ Bansal, N. & Raman, V. (1999), “Upper bounds for MaxSat: further improved”, in Aggarwal, A. & Pandu Rangan, C., Proc. 10th Conf. Algorithms and Computation, ISAAC’99, vol. 1741, Lecture Notes in Computer Science, Springer-Verlag, pp. 247–258 ; Gramm, Jens; Hirsch, Edward A.; Niedermeier, Rolf & Rossmanith, Peter (2003), “Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT”, Discrete Applied Mathematics 130 (2): 139–155, DOI 10.1016/S0166-218X(02)00402-X ; Kojevnikov, Arist & Kulikov, Alexander S. (2006), “A new approach to proving upper bounds for MAX-2-SAT”, Proc. 17th ACM-SIAM Symp. Discrete Algorithms, pp. 11–17, DOI 10.1145/1109557.1109559