Treewidth with a Quantifier Alternation Revisited

In this paper we take a closer look at the parameterized complexity of existsforall 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 existsforall SAT in time less than double-exponential in the input formula\u27s treewidth. More strongly, we establish the same bound with respect to the formula\u27s 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 existsforall 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\u27s primal vertex cover. - existsforall 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 existsforall SAT recently introduced by de Haan and Szeider, called exists_kforall SAT and existsforall_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