Treewidth with a Quantifier Alternation Revisited

Authors Michael Lampis, Valia Mitsou

Thumbnail PDF


  • Filesize: 458 kB
  • 12 pages

Document Identifiers

Author Details

Michael Lampis
Valia Mitsou

Cite AsGet BibTex

Michael Lampis and Valia Mitsou. Treewidth with a Quantifier Alternation Revisited. In 12th International Symposium on Parameterized and Exact Computation (IPEC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 89, pp. 26:1-26:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


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


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Albert Atserias and Sergi Oliva. Bounded-width QBF is pspace-complete. J. Comput. Syst. Sci., 80(7):1415-1429, 2014. Google Scholar
  2. Hubie Chen. Quantified constraint satisfaction and bounded treewidth. In ECAI, pages 161-165. IOS Press, 2004. Google Scholar
  3. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Inf. Comput., 85(1):12-75, 1990. Google Scholar
  4. Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michal Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015. Google Scholar
  5. Ronald de Haan and Stefan Szeider. Compendium of parameterized problems at higher levels of the polynomial hierarchy. Electronic Colloquium on Computational Complexity (ECCC), 21:143, 2014. Google Scholar
  6. Ronald de Haan and Stefan Szeider. Fixed-parameter tractable reductions to SAT. In SAT, volume 8561 of Lecture Notes in Computer Science, pages 85-102. Springer, 2014. Google Scholar
  7. Ronald de Haan and Stefan Szeider. Parameterized complexity classes beyond para-np. J. Comput. Syst. Sci., 87:16-57, 2017. Google Scholar
  8. Holger Dell, Eun Jung Kim, Michael Lampis, Valia Mitsou, and Tobias Mömke. Complexity and approximability of parameterized max-csps. In IPEC, volume 43 of LIPIcs, pages 294-306. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  9. Eduard Eiben, Robert Ganian, and Sebastian Ordyniak. Using decomposition-parameters for QBF: mind the prefix! In AAAI, pages 964-970. AAAI Press, 2016. Google Scholar
  10. Markus Frick and Martin Grohe. The complexity of first-order and monadic second-order logic revisited. Ann. Pure Appl. Logic, 130(1-3):3-31, 2004. Google Scholar
  11. Robert Ganian. Twin-cover: Beyond vertex cover in parameterized algorithmics. In IPEC, volume 7112 of Lecture Notes in Computer Science, pages 259-271. Springer, 2011. Google Scholar
  12. Robert Ganian, Petr Hlinený, Jaroslav Nesetril, Jan Obdrzálek, Patrice Ossona de Mendez, and Reshma Ramadurai. When trees grow low: Shrubs and fast MSO1. In MFCS, volume 7464 of Lecture Notes in Computer Science, pages 419-430. Springer, 2012. Google Scholar
  13. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001. Google Scholar
  14. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001. Google Scholar
  15. Michael Lampis. Algorithmic meta-theorems for restrictions of treewidth. Algorithmica, 64(1):19-37, 2012. Google Scholar
  16. Michael Lampis. Model checking lower bounds for simple graphs. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  17. Dániel Marx and Valia Mitsou. Double-exponential and triple-exponential bounds for choosability problems parameterized by treewidth. In ICALP, volume 55 of LIPIcs, pages 28:1-28:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  18. Sebastian Ordyniak. Private communication, 2017. Google Scholar
  19. Sebastian Ordyniak, Daniël Paulusma, and Stefan Szeider. Satisfiability of acyclic and almost acyclic CNF formulas. Theor. Comput. Sci., 481:85-99, 2013. Google Scholar
  20. Guoqiang Pan and Moshe Y. Vardi. Fixed-parameter hierarchies inside PSPACE. In LICS, pages 27-36. IEEE Computer Society, 2006. Google Scholar
  21. Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider. Model counting for CNF formulas of bounded modular treewidth. Algorithmica, 76(1):168-194, 2016. Google Scholar
  22. Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider. Model counting for CNF formulas of bounded modular treewidth. Algorithmica, 76(1):168-194, 2016. Google Scholar
  23. Sigve Hortemo Sæther, Jan Arne Telle, and Martin Vatshelle. Solving #sat and MAXSAT by dynamic programming. J. Artif. Intell. Res., 54:59-82, 2015. Google Scholar
  24. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010. Google Scholar
  25. Marko Samer and Stefan Szeider. Constraint satisfaction with bounded treewidth revisited. J. Comput. Syst. Sci., 76(2):103-114, 2010. Google Scholar
  26. Larry J. Stockmeyer. The polynomial-time hierarchy. Theor. Comput. Sci., 3(1):1-22, 1976. Google Scholar