The aim of this study is to present a wide range of variants of Planar 3–SAT, to show their various use in many fields of computer science, and to identify their characteristics.

In 1977, David Lichtenstein introduced in his master thesis the concept of planar Boolean formulas. The motivation was to have an easier way to prove NP–completeness of properties for general graphs on their planar derivatives. Previously, the common approach was to first prove the NP–completeness for general graphs and then adjust the proof for planar graphs. This mainly involves the construction of complicated crossover boxes where two edges intersect. With Lichtenstein’s definition of Planar 3–SAT and its proof of NP–completeness he accomplished a new and often easier way to show NP-completeness for properties of planar graphs. It also opens the way for many variants of Planar 3–SAT and their usefulness for the study of computational complexity.

The idea of Planar 3–SAT is to restrict 3–SAT to Boolean formulas with some property that can be easily mapped to planar graphs. For that each Boolean formula φ in 3–CNF is associated with a graph. This graph consists of vertices for each variable and for each clause in φ. An edge is put between a variable-vertex and a clause-vertex if the clause contains a literal of the variable. Additionally the variable-vertices are connected with edges in a circular order.

The thesis concludes with some open problems and a categorization of the presented variants.