Planar 3-SAT with a clause/variable cycle

Alexander Pilz

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Abstract

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, di erent 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.

Original languageEnglish
Title of host publication16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018
PublisherSchloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH
Pages311-3113
Number of pages2803
Volume101
ISBN (Electronic)9783959770682
DOIs
Publication statusPublished - 1 Jun 2018
Externally publishedYes
Event16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018 - Malmo, Sweden
Duration: 18 Jun 201820 Jun 2018

Conference

Conference16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018
CountrySweden
CityMalmo
Period18/06/1820/06/18

Fingerprint

Hamiltonians
Computational complexity

Keywords

  • 1-in-3-SAT
  • Phrases 3-SAT
  • Planar graph

ASJC Scopus subject areas

  • Software

Cite this

Pilz, A. (2018). Planar 3-SAT with a clause/variable cycle. In 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018 (Vol. 101, pp. 311-3113). Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH. https://doi.org/10.4230/LIPIcs.SWAT.2018.31

Planar 3-SAT with a clause/variable cycle. / Pilz, Alexander.

16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018. Vol. 101 Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH, 2018. p. 311-3113.

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Pilz, A 2018, Planar 3-SAT with a clause/variable cycle. in 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018. vol. 101, Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH, pp. 311-3113, 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018, Malmo, Sweden, 18/06/18. https://doi.org/10.4230/LIPIcs.SWAT.2018.31
Pilz A. Planar 3-SAT with a clause/variable cycle. In 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018. Vol. 101. Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH. 2018. p. 311-3113 https://doi.org/10.4230/LIPIcs.SWAT.2018.31
Pilz, Alexander. / Planar 3-SAT with a clause/variable cycle. 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018. Vol. 101 Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH, 2018. pp. 311-3113
@inproceedings{323eddab71fc448680d4a76223cae6fc,
title = "Planar 3-SAT with a clause/variable cycle",
abstract = "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, di erent 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{\"o}cker, and Dorn on the complexity of this problem variant in a surprising way.",
keywords = "1-in-3-SAT, Phrases 3-SAT, Planar graph",
author = "Alexander Pilz",
year = "2018",
month = "6",
day = "1",
doi = "10.4230/LIPIcs.SWAT.2018.31",
language = "English",
volume = "101",
pages = "311--3113",
booktitle = "16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018",
publisher = "Schloss Dagstuhl, Leibniz-Zentrum f{\"u} Informatik GmbH",
address = "Germany",

}

TY - GEN

T1 - Planar 3-SAT with a clause/variable cycle

AU - Pilz, Alexander

PY - 2018/6/1

Y1 - 2018/6/1

N2 - 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, di erent 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.

AB - 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, di erent 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.

KW - 1-in-3-SAT

KW - Phrases 3-SAT

KW - Planar graph

UR - http://www.scopus.com/inward/record.url?scp=85049024922&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.SWAT.2018.31

DO - 10.4230/LIPIcs.SWAT.2018.31

M3 - Conference contribution

VL - 101

SP - 311

EP - 3113

BT - 16th Scandinavian Symposium and Workshops on Algorithm Theory, SWAT 2018

PB - Schloss Dagstuhl, Leibniz-Zentrum fü Informatik GmbH

ER -