Planar 3-SAT with a Clause/Variable Cycle

Author Alexander Pilz

Thumbnail PDF


  • Filesize: 0.66 MB
  • 13 pages

Document Identifiers

Author Details

Alexander Pilz
  • Department of Computer Science, ETH Zürich. Zürich, Switzerland

Cite AsGet BibTex

Alexander Pilz. Planar 3-SAT with a Clause/Variable Cycle. In 16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 101, pp. 31:1-31:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


In the Planar 3-SAT problem, we are given a 3-SAT formula together with its incidence graph, which is planar, and are asked whether this formula is satisfiable. Since Lichtenstein's proof that this problem is NP-complete, it has been used as a starting point for a large number of reductions. In the course of this research, different restrictions on the incidence graph of the formula have been devised, for which the problem also remains hard. In this paper, we investigate the restriction in which we require that the incidence graph is augmented by the edges of a Hamiltonian cycle that first passes through all variables and then through all clauses, in a way that the resulting graph is still planar. We show that the problem of deciding satisfiability of a 3-SAT formula remains NP-complete even if the incidence graph is restricted in that way and the Hamiltonian cycle is given. This complements previous results demanding cycles only through either the variables or clauses. The problem remains hard for monotone formulas and instances with exactly three distinct variables per clause. In the course of this investigation, we show that monotone instances of Planar 3-SAT with three distinct variables per clause are always satisfiable, thus settling the question by Darmann, Döcker, and Dorn on the complexity of this problem variant in a surprising way.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • 3-SAT
  • 1-in-3-SAT
  • planar graph


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Oswin Aichholzer, Wolfgang Mulzer, and Alexander Pilz. Flip distance between triangulations of a simple polygon is np-complete. Discrete & Computational Geometry, 54(2):368-389, 2015. URL:
  2. Greg Aloupis, Erik D. Demaine, Alan Guo, and Giovanni Viglietta. Classic nintendo games are (computationally) hard. Theor. Comput. Sci., 586:135-160, 2015. URL:
  3. Kenneth Appel and Wolfgang Haken. Every Planar Map is Four-Colorable. Number 98 in Contemporary Mathematics. AMS, 1989. With the collaboration of J. Koch. Google Scholar
  4. Hans L. Bodlaender. A partial k-arboretum of graphs with bounded treewidth. Theor. Comput. Sci., 209(1-2):1-45, 1998. URL:
  5. Andreas Darmann, Janosch Döcker, and Britta Dorn. On planar variants of the monotone satisfiability problem with bounded variable appearances. CoRR, abs/1604.05588, 2016. URL:
  6. Andreas Darmann, Janosch Döcker, and Britta Dorn. The monotone satisfiability problem with bounded variable appearances. Int. J. Foundations Comp. Sci., 2017. To appear. Google Scholar
  7. Mark de Berg and Amirali Khosravi. Optimal binary space partitions for segments in the plane. Int. J. Comput. Geometry Appl., 22(3):187-206, 2012. URL:
  8. Hubert de Fraysseix, Patrice Ossona de Mendez, and János Pach. A left-first search algorithm for planar graphs. Discrete & Computational Geometry, 13:459-468, 1995. URL:
  9. Hubert de Fraysseix, János Pach, and Richard Pollack. How to draw a planar graph on a grid. Combinatorica, 10(1):41-51, 1990. URL:
  10. Erik Demaine. Algorithmic lower bounds: Fun with hardness proofs; Lecture 7. Scribe: Quanquan Liu, Jeffrey Bosboom. Retrieved June 21, 2017.
  11. Michael R. Fellows, Jan Kratochvíl, Matthias Middendorf, and Frank Pfeiffer. The complexity of induced minors and related problems. Algorithmica, 13(3):266-282, 1995. URL:
  12. Eldar Fischer, Johann A. Makowsky, and Elena V. Ravve. Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Applied Mathematics, 156(4):511-529, 2008. URL:
  13. Philip Hall. On representatives of subsets. J. London Math. Soc., s1-10(1):26-30, 1935. Google Scholar
  14. John E. Hopcroft and Richard M. Karp. An n^5/2 algorithm for maximum matchings in bipartite graphs. SIAM J. Comput., 2(4):225-231, 1973. URL:
  15. Harry B. Hunt III, Madhav V. Marathe, Venkatesh Radhakrishnan, and Richard Edwin Stearns. The complexity of planar counting problems. SIAM J. Comput., 27(4):1142-1167, 1998. URL:
  16. Sanjeev Khanna and Rajeev Motwani. Towards a syntactic characterization of PTAS. In Gary L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 329-337. ACM, 1996. URL:
  17. Donald E. Knuth. Nested satisfiability. Acta Inf., 28(1):1-6, 1990. URL:
  18. Donald E. Knuth and Arvind Raghunathan. The problem of compatible representatives. SIAM J. Discret. Math., 5(3):422-427, 1992. Google Scholar
  19. Jan Kratochvíl and Mirko Krivánek. Satisfiability of co-nested formulas. Acta Inf., 30(4):397-403, 1993. URL:
  20. Jan Kratochvíl, Anna Lubiw, and Jaroslav Nesetril. Noncrossing subgraphs in topological layouts. SIAM J. Discrete Math., 4(2):223-244, 1991. URL:
  21. David Lichtenstein. Planar formulae and their uses. SIAM J. Comput., 11:329-343, 1982. Google Scholar
  22. Anthony Mansfield. Determining the thickness of graphs is NP-hard. Math. Proc. Cambridge Phil. Soc., 93(01):9-23, 1983. Google Scholar
  23. Bernard M. E. Moret. Planar NAE3SAT is in P. SIGACT News, 19(2):51-54, 1988. Google Scholar
  24. Wolfgang Mulzer and Günter Rote. Minimum-weight triangulation is np-hard. J. ACM, 55(2):11:1-11:29, 2008. URL:
  25. Neil Robertson, Daniel P. Sanders, Paul D. Seymour, and Robin Thomas. Efficiently four-coloring planar graphs. In Gary L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 571-575. ACM, 1996. URL:
  26. Walter Schnyder. Embedding planar graphs on the grid. In David S. Johnson, editor, Proceedings of the First Annual ACM-SIAM Symposium on Discrete Algorithms, 22-24 January 1990, San Francisco, California., pages 138-148. SIAM, 1990. URL:
  27. Simon Tippenhauer. On planar 3-SAT and its variants. Master’s thesis, Freie Universität Berlin, 2016. Google Scholar
  28. Craig A. Tovey. A simplified np-complete satisfiability problem. Discrete Applied Mathematics, 8(1):85-89, 1984. URL:
  29. Salil P. Vadhan. The complexity of counting in sparse, regular, and planar graphs. SIAM J. Comput., 31(2):398-427, 2001. URL: