License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.IPEC.2017.26
URN: urn:nbn:de:0030-drops-85512
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8551/
Go to the corresponding LIPIcs Volume Portal

Lampis, Michael ; Mitsou, Valia

Treewidth with a Quantifier Alternation Revisited

pdf-format:
LIPIcs-IPEC-2017-26.pdf (0.4 MB)

Abstract

In this paper we take a closer look at the parameterized complexity of \exists\forall SAT, the prototypical complete problem of the class Sigma_2^p, the second level of the polynomial hierarchy. We provide a number of tight fine-grained bounds on the complexity of this problem and its variants with respect to the most important structural graph parameters. Specifically, we show the following lower bounds (assuming the ETH):

- It is impossible to decide \exists\forall SAT in time less than double-exponential in the input formula's treewidth. More strongly, we establish the same bound with respect to the formula's primal vertex cover, a much more restrictive measure. This lower bound, which matches the performance of known algorithms, shows that the degeneration of the performance of treewidth-based algorithms to a tower of exponentials already begins in problems with one quantifier alternation.

- For the more general \exists\forall CSP problem over a non-boolean domain of size B, there is no algorithm running in time 2^{B^{o(vc)}}, where vc is the input's primal vertex cover.

- \exists\forall SAT is already NP-hard even when the input formula has constant modular treewidth (or clique-width), indicating that dense graph parameters are less useful for problems in Sigma_2^p.

- For the two weighted versions of \exists\forall SAT recently introduced by de Haan and Szeider, called \exists_k\forall SAT and \exists\forall_k SAT, we give tight upper and lower bounds parameterized by treewidth (or primal vertex cover) and the weight k. Interestingly, the complexity of these two problems turns out to be quite different: one is double-exponential in treewidth, while the other is double-exponential in k.

We complement the above negative results by showing a double-exponential FPT algorithm for QBF parameterized by vertex cover, showing that for this parameter the complexity never goes beyond double-exponential, for any number of quantifier alternations.

BibTeX - Entry

@InProceedings{lampis_et_al:LIPIcs:2018:8551,
  author =	{Michael Lampis and Valia Mitsou},
  title =	{{Treewidth with a Quantifier Alternation Revisited}},
  booktitle =	{12th International Symposium on Parameterized and Exact Computation (IPEC 2017)},
  pages =	{26:1--26:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-051-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{89},
  editor =	{Daniel Lokshtanov and Naomi Nishimura},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8551},
  URN =		{urn:nbn:de:0030-drops-85512},
  doi =		{10.4230/LIPIcs.IPEC.2017.26},
  annote =	{Keywords: Treewidth, Exponential Time Hypothesis, Quantified SAT}
}

Keywords: Treewidth, Exponential Time Hypothesis, Quantified SAT
Collection: 12th International Symposium on Parameterized and Exact Computation (IPEC 2017)
Issue Date: 2018
Date of publication: 02.03.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI