Lampis, Michael ;
Mitsou, Valia
Treewidth with a Quantifier Alternation Revisited
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 finegrained 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 doubleexponential 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 treewidthbased algorithms to a tower of exponentials already begins in problems with one quantifier alternation.
 For the more general \exists\forall CSP problem over a nonboolean 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 NPhard even when the input formula has constant modular treewidth (or cliquewidth), 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 doubleexponential in treewidth, while the other is doubleexponential in k.
We complement the above negative results by showing a doubleexponential FPT algorithm for QBF parameterized by vertex cover, showing that for this parameter the complexity never goes beyond doubleexponential, 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:126:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770514},
ISSN = {18688969},
year = {2018},
volume = {89},
editor = {Daniel Lokshtanov and Naomi Nishimura},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2018/8551},
URN = {urn:nbn:de:0030drops85512},
doi = {10.4230/LIPIcs.IPEC.2017.26},
annote = {Keywords: Treewidth, Exponential Time Hypothesis, Quantified SAT}
}
02.03.2018
Keywords: 

Treewidth, Exponential Time Hypothesis, Quantified SAT 
Seminar: 

12th International Symposium on Parameterized and Exact Computation (IPEC 2017)

Issue date: 

2018 
Date of publication: 

02.03.2018 