Abstract
In the Planar 3SAT problem, we are given a 3SAT 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 NPcomplete, 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 3SAT formula remains NPcomplete 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 3SAT 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.
BibTeX  Entry
@InProceedings{pilz:LIPIcs:2018:8857,
author = {Alexander Pilz},
title = {{Planar 3SAT with a Clause/Variable Cycle}},
booktitle = {16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018)},
pages = {31:131:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770682},
ISSN = {18688969},
year = {2018},
volume = {101},
editor = {David Eppstein},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8857},
URN = {urn:nbn:de:0030drops88571},
doi = {10.4230/LIPIcs.SWAT.2018.31},
annote = {Keywords: 3SAT, 1in3SAT, planar graph}
}
Keywords: 

3SAT, 1in3SAT, planar graph 
Seminar: 

16th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2018) 
Issue Date: 

2018 
Date of publication: 

30.05.2018 