  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 can be 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, as well as for instances with
exactly three distinct variables per clause. In the course of this
investigation, we show that monotone instances of Planar 3-SAT with exactly
three distinct variables per clause are always satisfiable, thus settling the
question by Darmann, D\"ocker, and Dorn on the complexity of this problem
variant in a surprising way.
