Planar SAT

Boolean satisfiability problem restricted to a planar incidence graph
(Learn how and when to remove this message)
Graph of the formula (x_1 or not x_2) and (not x_1 or x_2 or not x_3)
Example of a planar SAT problem. The black edges correspond to non-inverted variables and the red edges correspond to inverted variables.

In computer science, the planar 3-satisfiability problem (abbreviated PLANAR 3SAT or PL3SAT) is an extension of the classical Boolean 3-satisfiability problem to a planar incidence graph. In other words, it asks whether the variables of a given Boolean formula—whose incidence graph consisting of variables and clauses can be embedded on a plane—can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

Like 3SAT, PLANAR-SAT is NP-complete, and is commonly used in reductions.

Definition

Every 3SAT problem can be converted to an incidence graph in the following manner: For every variable v i {\displaystyle v_{i}} , the graph has one corresponding node v i {\displaystyle v_{i}} , and for every clause c j {\displaystyle c_{j}} , the graph has one corresponding node c j . {\displaystyle c_{j}.} An edge ( v i , c j ) {\displaystyle (v_{i},c_{j})} is created between variable v i {\displaystyle v_{i}} and clause c j {\displaystyle c_{j}} whenever v i {\displaystyle v_{i}} or ¬ v i {\displaystyle \lnot v_{i}} is in c j {\displaystyle c_{j}} . Positive and negative literals are distinguished using edge colorings.

The formula is satisfiable if and only if there is a way to assign TRUE or FALSE to each variable node such that every clause node is connected to at least one TRUE by a positive edge or FALSE by a negative edge.

A planar graph is a graph that can be drawn on the plane in a way such that no two of its edges cross each other. Planar 3SAT is a subset of 3SAT in which the incidence graph of the variables and clauses of a Boolean formula is planar. It is important because it is a restricted variant, and is still NP-complete. Many problems (for example games and puzzles) cannot represent non-planar graphs. Hence, Planar 3SAT provides a way to prove those problems to be NP-hard.

Proof of NP-completeness

Graph with black and red edges
Left side is a crossing; right side is the crossover gadget. The small dots represent clauses. The black and red edges correspond to non-inverted and inverted variables respectively.

The following proof sketch follows the proof of D. Lichtenstein.[1]

Trivially, PLANAR 3SAT is in NP. It is thus sufficient to show that it is NP-hard via reduction from 3SAT.

This proof makes use of the fact that ( ¬ a ¬ b c ) ( a ¬ c ) ( b ¬ c ) {\displaystyle (\lnot a\lor \lnot b\lor c)\land (a\lor \lnot c)\land (b\lor \lnot c)} is equivalent to ( a b ) c {\displaystyle (a\land b)\leftrightarrow c} and that ( a ¬ b ) ( ¬ a b ) {\displaystyle (a\lor \lnot b)\land (\lnot a\lor b)} is equivalent to a b {\displaystyle a\leftrightarrow b} .

First, draw the incidence graph of the 3SAT formula. Since no two variables or clauses are connected, the resulting graph will be bipartite. Suppose the resulting graph is not planar. For every crossing of edges (a, c1) and (b, c2), introduce nine new variables a1, b1, α, β, γ, δ, ξ, a2, b2, and replace every crossing of edges with a crossover gadget shown in the diagram. It consists of the following new clauses:

( ¬ a 2 ¬ b 2 α ) ( a 2 ¬ α ) ( b 2 ¬ α ) , i.e., a 2 b 2 α ( ¬ a 2 b 1 β ) ( a 2 ¬ β ) ( ¬ b 1 ¬ β ) , i.e., a 2 ¬ b 1 β ( a 1 b 1 γ ) ( ¬ a 1 ¬ γ ) ( ¬ b 1 ¬ γ ) , i.e., ¬ a 1 ¬ b 1 γ ( a 1 ¬ b 2 δ ) ( ¬ a 1 ¬ δ ) ( b 2 ¬ δ ) , i.e., ¬ a 1 b 2 δ ( α β ξ ) ( γ δ ¬ ξ ) , i.e., α β γ δ ( ¬ α ¬ β ) ( ¬ β ¬ γ ) ( ¬ γ ¬ δ ) ( ¬ δ ¬ α ) , ( a 2 ¬ a ) ( a ¬ a 2 ) ( b 2 ¬ b ) ( b ¬ b 2 ) , i.e., a a 2 ,   b b 2 {\displaystyle {\begin{array}{ll}(\lnot a_{2}\lor \lnot b_{2}\lor \alpha )\land (a_{2}\lor \lnot \alpha )\land (b_{2}\lor \lnot \alpha ),&\quad {\text{i.e.,}}\quad a_{2}\land b_{2}\leftrightarrow \alpha \\(\lnot a_{2}\lor b_{1}\lor \beta )\land (a_{2}\lor \lnot \beta )\land (\lnot b_{1}\lor \lnot \beta ),&\quad {\text{i.e.,}}\quad a_{2}\land \lnot b_{1}\leftrightarrow \beta \\(a_{1}\lor b_{1}\lor \gamma )\land (\lnot a_{1}\lor \lnot \gamma )\land (\lnot b_{1}\lor \lnot \gamma ),&\quad {\text{i.e.,}}\quad \lnot a_{1}\land \lnot b_{1}\leftrightarrow \gamma \\(a_{1}\lor \lnot b_{2}\lor \delta )\land (\lnot a_{1}\lor \lnot \delta )\land (b_{2}\lor \lnot \delta ),&\quad {\text{i.e.,}}\quad \lnot a_{1}\land b_{2}\leftrightarrow \delta \\(\alpha \lor \beta \lor \xi )\land (\gamma \lor \delta \lor \lnot \xi ),&\quad {\text{i.e.,}}\quad \alpha \lor \beta \lor \gamma \lor \delta \\(\lnot \alpha \lor \lnot \beta )\land (\lnot \beta \lor \lnot \gamma )\land (\lnot \gamma \lor \lnot \delta )\land (\lnot \delta \lor \lnot \alpha ),&\\(a_{2}\lor \lnot a)\land (a\lor \lnot a_{2})\land (b_{2}\lor \lnot b)\land (b\lor \lnot b_{2}),&\quad {\text{i.e.,}}\quad a\leftrightarrow a_{2},~b\leftrightarrow b_{2}\\\end{array}}}

If the edge (a, c1) is inverted in the original graph, (a1, c1) should be inverted in the crossover gadget. Similarly if the edge (b, c2) is inverted in the original, (b1, c2) should be inverted.

One can easily show that these clauses are satisfiable if and only if a a 1 {\displaystyle a\leftrightarrow a_{1}} and b b 1 {\displaystyle b\leftrightarrow b_{1}} .

This algorithm shows that it is possible to convert each crossing into its planar equivalent using only a constant amount of new additions. Since the number of crossings is polynomial in terms of the number of clauses and variables, the reduction is polynomial.[2]

Variants and related problems

Reductions

Logic puzzles

Reduction from Planar SAT is a commonly used method in NP-completeness proofs of logic puzzles. Examples of these include Fillomino,[10] Nurikabe,[11] Shakashaka,[12] Tatamibari,[13] and Tentai Show.[14] These proofs involve constructing gadgets that can simulate wires carrying signals (Boolean values), input and output gates, signal splitters, NOT gates and AND (or OR) gates in order to represent the planar embedding of any Boolean circuit. Since the circuits are planar, crossover of wires do not need to be considered.

Flat folding of fixed-angle chains

This is the problem of deciding whether a polygonal chain with fixed edge lengths and angles has a planar configuration without crossings. It has been proven to be strongly NP-hard via a reduction from planar monotone rectilinear 3SAT.[15]

Minimum edge-length partition

This is the problem of partitioning a polygon into simpler polygons such that the total length of all edges used in the partition is as small as possible.

When the figure is a rectilinear polygon and it should be partitioned into rectangles, and the polygon is hole-free, then the problem is polynomial. But if it contains holes (even degenerate holes—single points), the problem is NP-hard, by reduction from Planar SAT. The same holds if the figure is any polygon and it should be partitioned into convex figures.[16]

A related problem is minimum-weight triangulation - finding a triangulation of minimal total edge length. The decision version of this problem is proven to be NP-complete via a reduction from a variant of Planar 1-in-3SAT.[17]

References

  1. ^ a b c Lichtenstein, David (1982-05-01). "Planar Formulae and Their Uses". SIAM Journal on Computing. 11 (2): 329–343. doi:10.1137/0211025. ISSN 0097-5397.
  2. ^ Demaine, Eric (2015). "7. Planar SAT". MIT Open CourseWare.
  3. ^ Raghunathan, Arvind; Knuth, Donald E. (1992). "The problem of compatible representatives". SIAM J. Discrete Math. 5 (3): 422–427. arXiv:cs/9301116. Bibcode:1993cs........1116K. doi:10.1137/0405033. S2CID 9974756.
  4. ^ De Berg, Mark; Khosravi, Amirali (2010). "Optimal Binary Space Partitions in the Plane". Computing and Combinatorics. Lecture Notes in Computer Science. Vol. 6196. pp. 216–225. doi:10.1007/978-3-642-14031-0_25. ISBN 978-3-642-14030-3.
  5. ^ Agarwal, Pankaj K.; Aronov, Boris; Geft, Tzvika; Halperin, Dan (2021). "On Two-Handed Planar Assembly Partitioning with Connectivity Constraints". Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA): 1740–1756. arXiv:2009.12369. doi:10.1137/1.9781611976465.105. ISBN 978-1-61197-646-5.
  6. ^ Dyer, M.E; Frieze, A.M (June 1986). "Planar 3DM is NP-complete". Journal of Algorithms. 7 (2): 174–184. doi:10.1016/0196-6774(86)90002-7.
  7. ^ Mulzer, Wolfgang; Rote, Günter (2008-05-15). "Minimum-weight triangulation is NP-hard". Journal of the ACM. 55 (2): 11:1–11:29. arXiv:cs/0601002. doi:10.1145/1346330.1346336. ISSN 0004-5411. S2CID 1658062.
  8. ^ Moret, B. M. E. (June 1988). "Planar NAE3SAT is in P". SIGACT News. 19 (2): 51–54. doi:10.1145/49097.49099. ISSN 0163-5700. S2CID 17219595.
  9. ^ Demaine, Erik (2015). "6. Circuit SAT". Youtube.
  10. ^ Yato, Takauki (2003). Complexity and Completeness of Finding Another Solution and its Application to Puzzles. CiteSeerX 10.1.1.103.8380.
  11. ^ Holzer, Markus; Klein, Andreas; Kutrib, Martin (2004). "On The NP-Completeness of The NURIKABE Pencil Puzzle and Variants Thereof" (PDF). Proceedings of the 3rd International Conference on Fun with Algorithms. S2CID 16082806. Archived from the original (PDF) on 2020-02-11.
  12. ^ Demaine, Erik D.; Okamoto, Yoshio; Uehara, Ryuhei; Uno, Yushi (2014), "Computational complexity and an integer programming model of Shakashaka" (PDF), IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, E97-A (6): 1213–1219, Bibcode:2014IEITF..97.1213D, doi:10.1587/transfun.E97.A.1213, hdl:10119/12147
  13. ^ Adler, Aviv; Bosboom, Jeffrey; Demaine, Erik D.; Demaine, Martin L.; Liu, Quanquan C.; Lynch, Jayson (7 May 2020). "Tatamibari is NP-complete". arXiv:2003.08331 [cs.CC].
  14. ^ Fertin, Guillaume; Jamshidi, Shahrad; Komusiewicz, Christian (June 2015). "Towards an Algorithmic Guide to Spiral Galaxies". Theoretical Computer Science. 586: 26–39. doi:10.1016/j.tcs.2015.01.051. S2CID 766372. Retrieved 18 August 2021.
  15. ^ Demaine, Erik D.; Eisenstat, Sarah (2011). "Flattening Fixed-Angle Chains is Strongly NP-Hard". In Dehne, Frank; Iacono, John; Sack, Jörg-Rüdiger (eds.). Algorithms and Data Structures. Lecture Notes in Computer Science. Vol. 6844. Springer Berlin Heidelberg. pp. 314–325. doi:10.1007/978-3-642-22300-6_27. ISBN 9783642223006.
  16. ^ Lingas, Andrzej; Pinter, Ron Y.; Rivest, Ronald L.; Shamir, Adi (1982). "Minimum edge length partitioning of rectilinear polygons" (PDF). Proc. 20th Allerton Conf. Commun. Control Comput: 53–63.
  17. ^ Mulzer, Wolfgang; Rote, Günter (May 2008). "Minimum-weight Triangulation is NP-hard". J. ACM. 55 (2): 11:1–11:29. arXiv:cs/0601002. doi:10.1145/1346330.1346336. ISSN 0004-5411. S2CID 1658062.