摘要：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.
关键词：Treewidth; Exponential Time Hypothesis; Quantified SAT
Loading...
