Editing 2-satisfiability (section)

===Conflict-free placement of geometric objects===
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, the set of possible locations for each label is highly constrained, not only by the map itself (each label must be near the feature it labels, and must not obscure other features), but by each other: every two labels should avoid overlapping each other, for otherwise they would become illegible. In general, finding a label placement that obeys these constraints 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 label placement 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 that has a clause for each pair of labels that could overlap, preventing them from being assigned overlapping positions. If the labels are all congruent rectangles, the corresponding 2-satisfiability instance can be shown to have only linearly many constraints, leading to near-linear time algorithms for finding a labeling.<ref name="fw91">{{citation|first1=M.|last1=Formann|first2=F.|last2=Wagner|contribution=A packing problem with applications to lettering of maps|title=Proc. 7th ACM Symposium on Computational Geometry|year=1991|pages=281–288|doi=10.1145/109648.109680|isbn=978-0-89791-426-0|title-link=Symposium on Computational Geometry|s2cid=15740667}}.</ref> {{harvtxt|Poon|Zhu|Chin|1998}} describe a map labeling problem in which each label is a rectangle that may be placed in one of three positions with respect to a line segment that it labels: it may have the segment as one of its sides, or it may be centered on the segment. They represent these three positions using two binary variables in such a way that, again, testing the existence of a valid labeling becomes a 2-satisfiability problem.<ref>{{citation|first1=Chung Keung|last1=Poon|first2=Binhai|last2=Zhu|first3=Francis|last3=Chin|author3-link=Y. L. Chin|title=A polynomial time solution for labeling a rectilinear map|journal=[[Information Processing Letters]]|volume=65|issue=4|year=1998|pages=201–207|doi=10.1016/S0020-0190(98)00002-7}}.</ref>

{{harvtxt|Formann|Wagner|1991}} use 2-satisfiability as part of an [[approximation algorithm]] for the problem of finding square labels of the largest possible size for a given set of points, with the constraint that each label has one of its corners on the point that it labels. To find a labeling with a given size, they eliminate squares that, if doubled, would overlap another point, and they eliminate points that can be labeled in a way that cannot possibly overlap with another point's label. They show that these elimination rules cause the remaining points to have only two possible label placements per point, allowing a valid label placement (if one exists) to be found as the solution to a 2-satisfiability instance. By searching for the largest label size that leads to a solvable 2-satisfiability instance, they find a valid label placement whose labels are at least half as large as the optimal solution. That is, the [[approximation ratio]] of their algorithm is at most two.<ref name="fw91"/><ref>{{citation|first1=Frank|last1=Wagner|first2=Alexander|last2=Wolff|title=A practical map labeling algorithm|journal=[[Computational Geometry (journal)|Computational Geometry: Theory and Applications]]|volume=7|issue=5–6|year=1997|pages=387–404|doi=10.1016/S0925-7721(96)00007-7}}.</ref> Similarly, if each label is rectangular and must be placed in such a way that the point it labels is somewhere along its bottom edge, then using 2-satisfiability to find the largest label size for which there is a solution in which each label has the point on a bottom corner leads to an approximation ratio of at most two.<ref>{{citation|first1=Srinivas|last1=Doddi|first2=Madhav V.|last2=Marathe|first3=Andy|last3=Mirzaian|first4=Bernard M. E.|last4=Moret|first5=Binhai|last5=Zhu|contribution=Map labeling and its generalizations|title=Proc. 8th ACM-SIAM Symp. Discrete Algorithms (SODA)|year=1997|pages=148–157|contribution-url=http://portal.acm.org/citation.cfm?id=314250|isbn=978-0-89871-390-9|series=Soda '97}}.</ref>

Similar applications of 2-satisfiability have been made for other geometric placement problems. In [[graph drawing]], if the vertex locations are fixed and each edge must be drawn as a circular arc with one of two possible locations (for instance as an [[arc diagram]]), then the problem of choosing which arc to use for each edge in order to avoid crossings is a 2-satisfiability problem with a variable for each edge and a constraint for each pair of placements that would lead to a crossing. However, in this case it is possible to speed up the solution, compared to an algorithm that builds and then searches an explicit representation of the implication graph, by searching the graph [[implicit graph|implicitly]].<ref>{{citation|first1=Alon|last1=Efrat|first2=Cesim|last2=Erten|first3=Stephen G.|last3=Kobourov|title=Fixed-location circular arc drawing of planar graphs|journal=[[Journal of Graph Algorithms and Applications]]|volume=11|issue=1|pages=145–164|year=2007|url=http://jgaa.info/accepted/2007/EfratErtenKobourov2007.11.1.pdf|doi=10.7155/jgaa.00140}}.</ref>
In [[VLSI]] integrated circuit design, if a collection of modules must be connected by wires that can each bend at most once, then again there are two possible routes for the wires, and the problem of choosing which of these two routes to use, in such a way that all wires can be routed in a single layer of the circuit, can be solved as a 2-satisfiability instance.<ref>{{citation|first1=Raghunath|last1=Raghavan|first2= James|last2=Cohoon|first3=Sartaj|last3=Sahni|author3-link=Sartaj Sahni|title=Single bend wiring|journal=Journal of Algorithms|volume=7|issue=2|year=1986|pages=232–237|doi=10.1016/0196-6774(86)90006-4}}.</ref>

{{harvtxt|Boros|Hammer|Minoux|Rader|1999}} consider another VLSI design problem: the question of whether or not to mirror-reverse each module in a circuit design. This mirror reversal leaves the module's operations unchanged, but it changes the order of the points at which the input and output signals of the module connect to it, possibly changing how well the module fits into the rest of the design. Boros ''et al.'' consider a simplified version of the problem in which the modules have already been placed along a single linear channel, in which the wires between modules must be routed, and there is a fixed bound on the density of the channel (the maximum number of signals that must pass through any cross-section of the channel). 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.<ref>{{citation|first1=Endre|last1=Boros|first2=Peter Ladislaw|last2=Hammer|author2-link=Peter Ladislaw Hammer|first3=Michel|last3=Minoux|first4=David J. Jr.|last4=Rader|title=Optimal cell flipping to minimize channel density in VLSI design and pseudo-Boolean optimization|journal=[[Discrete Applied Mathematics]]|volume=90|issue=1–3|year=1999|pages=69–88|doi=10.1016/S0166-218X(98)00114-0}}.</ref>