Editing 2-satisfiability (section)

==Applications==

===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>

===Data clustering===
One way of [[data clustering|clustering a set of data points]] in a [[metric space]] into two clusters is to choose the clusters in such a way as to minimize the sum of the [[diameter]]s of the clusters, where the diameter of any single cluster is the largest distance between any two of its points. This is preferable to minimizing the maximum cluster size, which may lead to very similar points being assigned to different clusters. If the target diameters of the two clusters are known, a clustering that achieves those targets may be found by solving a 2-satisfiability instance. The instance has one variable per point, indicating whether that point belongs to the first cluster or the second cluster. Whenever any two points are too far apart from each other for both to belong to the same cluster, a clause is added to the instance that prevents this assignment.

The same method also can be used as a subroutine when the individual cluster diameters are unknown. To test whether a given sum of diameters can be achieved without knowing the individual cluster diameters, one may try all maximal pairs of target diameters that add up to at most the given sum, representing each pair of diameters as a 2-satisfiability instance and using a 2-satisfiability algorithm to determine whether that pair can be realized by a clustering. To find the optimal sum of diameters one may perform a binary search in which each step is a feasibility test of this type. The same approach also works to find clusterings that optimize other combinations than sums of the cluster diameters, and that use arbitrary dissimilarity numbers (rather than distances in a metric space) to measure the size of a cluster.<ref>{{citation|first1=P.|last1=Hansen|first2=B.|last2=Jaumard|author2-link= Brigitte Jaumard |title=Minimum sum of diameters clustering|journal=Journal of Classification|volume=4|issue=2|year=1987|pages=215–226|doi=10.1007/BF01896987|s2cid=120583429}}.</ref> The time bound for this algorithm is dominated by the time to solve a sequence of 2-satisfiability instances that are closely related to each other, and {{harvtxt|Ramnath|2004}} shows how to solve these related instances more quickly than if they were solved independently from each other, leading to a total time bound of {{math|''O''(''n''<sup>3</sup>)}} for the sum-of-diameters clustering problem.<ref>{{citation|first1=Sarnath|last1=Ramnath|title=Dynamic digraph connectivity hastens minimum sum-of-diameters clustering|journal=[[SIAM Journal on Discrete Mathematics]]|volume=18|issue=2|pages=272–286|year=2004|doi=10.1137/S0895480102396099}}.</ref>

===Scheduling===
{{harvtxt|Even|Itai|Shamir|1976}} consider a model of classroom scheduling  in which a set of ''n'' teachers must be scheduled to teach each of ''m'' cohorts of students. The number of hours per week that teacher <math>i</math> spends with cohort <math>j</math> is described by entry <math>R_{ij}</math> of a matrix <math>R</math> given as input to the problem, and each teacher also has a set of hours during which he or she is available to be scheduled. As they show, the problem is [[NP-complete]], even when each teacher has at most three available hours, but it can be solved as an instance of 2-satisfiability when each teacher only has two available hours. (Teachers with only a single available hour may easily be eliminated from the problem.) In this problem, each variable <math>v_{ij}</math> corresponds to an hour that teacher <math>i</math> must spend with cohort <math>j</math>, the assignment to the variable specifies whether that hour is the first or the second of the teacher's available hours, and there is a 2-satisfiability clause preventing any conflict of either of two types: two cohorts assigned to a teacher at the same time as each other, or one cohort assigned to two teachers at the same time.<ref name="EIS76"/>

{{harvtxt|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. In this problem, it is desirable to alternate home and away games to the extent possible, avoiding "breaks" in which a team plays two home games in a row or two away games in a row. At most two teams can avoid breaks entirely, alternating between home and away games; no other team can have the same home-away schedule as these two, because then it would be unable to play the team with which it had the same schedule. Therefore, an optimal schedule has two breakless teams and a single break for every other team. Once one of the breakless teams is chosen, one can set up a 2-satisfiability problem in which each variable represents the home-away assignment for a single team in a single game, and the constraints enforce the properties that any two teams have a consistent assignment for their games, that each team have at most one break before and at most one break after the game with the breakless team, and that no team has two breaks. Therefore, testing whether a schedule admits a solution with the optimal number of breaks can be done by solving a linear number of 2-satisfiability problems, one for each choice of the breakless team. A similar technique also allows finding schedules in which every team has a single break, and maximizing rather than minimizing the number of breaks (to reduce the total mileage traveled by the teams).<ref>{{citation|first1=Ryuhei|last1=Miyashiro|first2=Tomomi|last2=Matsui|title=A polynomial-time algorithm to find an equitable home–away assignment|journal=Operations Research Letters|volume=33|issue=3|year=2005|pages=235–241|doi=10.1016/j.orl.2004.06.004|citeseerx=10.1.1.64.240}}.</ref>

===Discrete tomography===
[[File:Nonogram_wiki.svg|thumb|Example of a nonogram puzzle.]]
[[Tomography]] is the process of recovering shapes from their cross-sections. In [[discrete tomography]], a simplified version of the problem that has been frequently studied, the shape to be recovered is a [[polyomino]] (a subset of the squares in the two-dimensional [[square lattice]]), and the cross-sections provide aggregate information about the sets of squares in individual rows and columns of the lattice. 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 [[pixel]]s 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. In other forms of digital tomography, even less information about each row or column is given: only the total number of squares, rather than the number and length of the blocks of squares. An equivalent version of the problem is that we must recover a given [[0-1 matrix]] given only the sums of the values in each row and in each column of the matrix.

Although there exist polynomial time algorithms to find a matrix having given row and column sums,<ref>{{citation|first=R. A.|last=Brualdi|author-link=Richard A. Brualdi|title=Matrices of zeros and ones with fixed row and column sum vectors|journal=Linear Algebra Appl.|volume=33|year=1980|pages=159–231|doi=10.1016/0024-3795(80)90105-6|doi-access=free}}.</ref> the solution may be far from unique: any submatrix in the form of a 2&nbsp;×&nbsp;2 [[identity matrix]] can be complemented without affecting the correctness of the solution. Therefore, researchers have searched for constraints on the shape to be reconstructed that can be used to restrict the space of solutions. For instance, one might assume that the shape is connected; however, testing whether there exists a connected solution is NP-complete.<ref>{{citation|first=G. J.|last=Woeginger|author-link= Gerhard J. Woeginger |title=The reconstruction of polyominoes from their orthogonal projections|series=Technical Report SFB-65|publisher=TU Graz|location=Graz, Austria|year=1996}}.</ref> An even more constrained version that is easier to solve is that the shape is [[orthogonal convexity|orthogonally convex]]: having a single contiguous block of squares in each row and column.
Improving several previous solutions, {{harvtxt|Chrobak|Dürr|1999}} showed how to reconstruct connected orthogonally convex shapes efficiently, using 2-SAT.<ref>{{citation|first1=Marek|last1=Chrobak|first2=Christoph|last2=Dürr|title=Reconstructing hv-convex polyominoes from orthogonal projections|journal=[[Information Processing Letters]]|volume=69|issue=6|year=1999|pages=283–289|doi=10.1016/S0020-0190(99)00025-3|arxiv=cs/9906021|bibcode=1999cs........6021D|s2cid=6799509}}.</ref> The idea of their solution is to guess the indexes of rows containing the leftmost and rightmost cells of the shape to be reconstructed, and then to set up a 2-satisfiability problem that tests whether there exists a shape consistent with these guesses and with the given row and column sums. They use four 2-satisfiability variables for each square that might be part of the given shape, one to indicate whether it belongs to each of four possible "corner regions" of the shape, and they use constraints that force these regions to be disjoint, to have the desired shapes, to form an overall shape with contiguous rows and columns, and to have the desired row and column sums. Their algorithm takes time {{math|O(''m''<sup>3</sup>''n'')}} where {{math|''m''}} is the smaller of the two dimensions of the input shape and {{math|''n''}} is the larger of the two dimensions.  The same method was later extended to orthogonally convex shapes that might be connected only diagonally instead of requiring orthogonal connectivity.<ref>{{citation|first1=Attila|last1=Kuba|first2=Emese|last2=Balogh|title=Reconstruction of convex 2D discrete sets in polynomial time|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=283|issue=1|year=2002|pages=223–242|doi=10.1016/S0304-3975(01)00080-9|doi-access=free}}; {{citation|first1=Sara|last1=Brunetti|first2=Alain|last2=Daurat|title=An algorithm reconstructing convex lattice sets|journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=304|issue=1–3|pages=35–57|year=2003|doi=10.1016/S0304-3975(03)00050-1|s2cid=2803842 |url=http://hal.archives-ouvertes.fr/docs/00/06/61/77/PDF/tomoqconv_els.pdf}}.</ref>

A part of a solver for full nonogram puzzles, {{harvs|last1=Batenburg|last2=Kosters|year=2008|year2=2009|txt}} used 2-satisfiability to combine information obtained from several other [[heuristic]]s. Given a partial solution to the puzzle, they use [[dynamic programming]] within each row or column to determine whether the constraints of that row or column force any of its squares to be white or black, and whether any two squares in the same row or column can be connected by an implication relation. 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. If either of these two heuristics determines the value of one of the squares, it is included in the partial solution and the same calculations are repeated. However, if both heuristics fail to set any squares, the implications found by both of them are combined into a 2-satisfiability problem and a 2-satisfiability solver is used to find squares whose value is fixed by the problem, after which the procedure is again repeated. This procedure may or may not succeed in finding a solution, but it is guaranteed to run in polynomial time. 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 {{harvtxt|Even|Itai|Shamir|1976}}<ref name="EIS76"/> are significantly more effective than the dynamic programming and flow heuristics without 2-satisfiability when applied to more difficult randomly generated nonograms.<ref>{{citation|first1=K. Joost|last1=Batenburg|first2=Walter A.|last2=Kosters|contribution=A reasoning framework for solving Nonograms|title=Combinatorial Image Analysis, 12th International Workshop, IWCIA 2008, Buffalo, NY, USA, April 7–9, 2008, Proceedings|series=Lecture Notes in Computer Science|volume=4958|year=2008|publisher=Springer-Verlag|pages=372–383|doi=10.1007/978-3-540-78275-9_33|isbn=978-3-540-78274-2|doi-access=free}}; {{citation|first1=K. Joost|last1=Batenburg|first2=Walter A.|last2=Kosters|title=Solving Nonograms by combining relaxations|journal=Pattern Recognition|volume=42|issue=8|year=2009|pages=1672–1683|doi=10.1016/j.patcog.2008.12.003|bibcode=2009PatRe..42.1672B |citeseerx=10.1.1.177.76}}.</ref>

===Renamable Horn satisfiability===
Next to 2-satisfiability, the other major subclass of satisfiability problems that can be solved in polynomial time is [[Horn-satisfiability]]. In this class of satisfiability problems, the input is again a formula in conjunctive normal form. It can have arbitrarily many literals per clause but at most one positive literal. {{harvtxt|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. A formula is ''renamable Horn'' when it is possible to put it into Horn form by replacing some variables by their negations. To do so, Lewis sets up a 2-satisfiability instance with one variable for each variable of the renamable Horn instance, where the 2-satisfiability variables indicate whether or not to negate the corresponding renamable Horn variables.
In order to produce a Horn instance, no two variables that appear in the same clause of the renamable Horn instance should appear positively in that clause; this constraint on a pair of variables is a 2-satisfiability constraint. By finding a satisfying assignment to the resulting 2-satisfiability instance, Lewis shows how to turn any renamable Horn instance into a Horn instance in polynomial time.<ref>{{citation
 | last = Lewis | first = Harry R. | author-link = Harry R. Lewis
 | doi = 10.1145/322047.322059
 | issue = 1
 | journal = [[Journal of the ACM]]
 | mr = 0468315
 | pages = 134–135
 | title = Renaming a set of clauses as a Horn set
 | volume = 25
 | year = 1978| s2cid = 3071958 | doi-access = free
 }}.</ref> By breaking up long clauses into multiple smaller clauses, and applying a linear-time 2-satisfiability algorithm, it is possible to reduce this to linear time.<ref>{{citation
 | last = Aspvall | first = Bengt
 | doi = 10.1016/0196-6774(80)90007-3
 | issue = 1
 | journal = Journal of Algorithms
 | mr = 578079
 | pages = 97–103
 | title = Recognizing disguised NR(1) instances of the satisfiability problem
 | volume = 1
 | year = 1980}}.</ref>

===Other applications===
2-satisfiability has also been applied to problems of recognizing [[undirected graph]]s that can be partitioned into an [[Independent set (graph theory)|independent set]] and a small number of [[complete bipartite graph|complete bipartite subgraphs]],<ref>{{citation|first1=Andreas|last1=Brandstädt|author1-link=Andreas Brandstädt|first2=Peter Ladislaw|last2=Hammer|author2-link=Peter Ladislaw Hammer|first3=Van Bang|last3=Le|first4=Vadim V.|last4=Lozin|title=Bisplit graphs|journal=[[Discrete Mathematics (journal)|Discrete Mathematics]]|volume=299|issue=1–3|year=2005|pages=11–32|doi=10.1016/j.disc.2004.08.046|doi-access=free}}.</ref> inferring business relationships among autonomous subsystems of the internet,<ref>{{citation|first1=Hao|last1=Wang|first2=Haiyong|last2=Xie|first3=Yang Richard|last3=Yang|first4=Avi|last4=Silberschatz|first5=Li Erran|last5=Li|first6=Yanbin|last6=Liu|title=13TH IEEE International Conference on Network Protocols (ICNP'05) |contribution=Stable egress route selection for interdomain traffic engineering: model and analysis|year=2005|pages=16–29|doi=10.1109/ICNP.2005.39|isbn=978-0-7695-2437-5|citeseerx=10.1.1.106.7345|s2cid=4332805}}.</ref> and reconstruction of [[evolutionary tree]]s.<ref>{{citation|first1=Eleazar|last1=Eskin|first2=Eran|last2=Halperin|first3=Richard M.|last3=Karp|author-link3=Richard Karp|title=Efficient reconstruction of haplotype structure via perfect phylogeny|journal=Journal of Bioinformatics and Computational Biology|year=2003|volume=1|issue=1|pages=1–20|doi=10.1142/S0219720003000174|pmid=15290779}}.</ref>