Abstract
We propose reductions to quantified Boolean formulas (QBF) as a new approach to showing fixed-parameter linear algorithms for problems parameterized by treewidth. We demonstrate the feasibility of this approach by giving new algorithms for several well-known problems from artificial intelligence that are in general complete for the second level of the polynomial hierarchy. By reduction from QBF we show that all resulting algorithms are essentially optimal in their dependence on the treewidth. Most of the problems that we consider were already known to be fixed-parameter linear by using Courcelle’s Theorem or dynamic programming, but we argue that our approach has clear advantages over these techniques: on the one hand, in contrast to Courcelle’s Theorem, we get concrete and tight guarantees for the runtime dependence on the treewidth. On the other hand, we avoid tedious dynamic programming and, after showing some normalization results for CNF-formulas, our upper bounds often boil down to a few lines.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
To give the reader an impression: \(2^{2^5} \approx 4.2\times 10^9\) and already \(2^{2^6} \approx 1.8\times 10^{19}\).
References
Arieli, O., Caminada, M.W.A.: A general QBF-based formalization of abstract argumentation theory. In: Verheij, B., Szeider, S., Woltran, S. (eds.) Computational Models of Argument, COMMA 2012, pp. 105–116 (2012)
Arnborg, S., Proskurowski, A.: Linear time algorithms for NP-hard problems restricted to partial k-trees. Discrete Appl. Math. 23(1), 11–24 (1989)
Atserias, A., Oliva, S.: Bounded-width QBF is PSPACE-complete. J. Comput. Syst. Sci. 80(7), 1415–1429 (2014)
Bodlaender, H.L.: A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput. 25(6), 1305–1317 (1996)
Bodlaender, H.L., Drange, P.G., Dregi, M.S., Fomin, F.V., Lokshtanov, D., Pilipczuk, M.: An o(c\({}^{\wedge }\)k n) 5-approximation algorithm for treewidth. In: 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, pp. 499–508 (2013)
Cadoli, M., Lenzerini, M.: The complexity of propositional closed world reasoning and circumscription. J. Comput. Syst. Sci. 48(2), 255–310 (1994)
Chen, H.: Quantified constraint satisfaction and bounded treewidth. In: de Mántaras, R.L., Saitta, L. (eds.) Proceedings of the 16th European Conference on Artificial Intelligence, ECAI 2004, pp. 161–165 (2004)
Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)
DIMACS: Satisfiability: Suggested Format. DIMACS Challenge. DIMACS (1993)
Dung, P.M.: On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artif. Intell. 77(2), 321–358 (1995)
Dunne, P.E.: Computational properties of argument systems satisfying graph-theoretic constraints. Artif. Intell. 171(10–15), 701–729 (2007)
Dunne, P.E., Bench-Capon, T.J.M.: Coherence in finite argument systems. Artif. Intell. 141(1/2), 187–203 (2002)
Dvorák, W., Pichler, R., Woltran, S.: Towards fixed-parameter tractable algorithms for abstract argumentation. Artif. Intell. 186, 1–37 (2012)
Egly, U., Woltran, S.: Reasoning in argumentation frameworks using quantified boolean formulas. In: Dunne, P.E., Bench-Capon, T.J.M. (eds.) Computational Models of Argument, COMMA 2006, pp. 133–144 (2006)
Eiben, E., Ganian, R., Ordyniak, S.: Using decomposition-parameters for QBF: mind the prefix! In: Schuurmans, D., Wellman, M.P. (eds.) Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, pp. 964–970 (2016)
Eiben, E., Ganian, R., Ordyniak, S.: Small resolution proofs for QBF using dependency treewidth. CoRR, abs/1711.02120 (2017)
Eiter, T., Gottlob, G.: Propositional circumscription and extended closed-world reasoning are \(\varPi ^{p}_2\)-complete. Theor. Comput. Sci. 114(2), 231–245 (1993)
Eiter, T., Gottlob, G.: The complexity of logic-based abduction. J. ACM 42(1), 3–42 (1995)
Fischer, E., Makowsky, J.A., Ravve, E.V.: Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Appl. Math. 156(4), 511–529 (2008)
Frick, M., Grohe, M.: The complexity of first-order and monadic second-order logic revisited. Ann. Pure Appl. Logic 130(1–3), 3–31 (2004)
Gottlob, G., Pichler, R., Wei, F.: Bounded treewidth as a key to tractability of knowledge representation and reasoning. Artif. Intell. 174(1), 105–132 (2010)
Ignatiev, A., Previti, A., Liffiton, M., Marques-Silva, J.: Smallest MUS extraction with minimal hitting set dualization. In: Pesant, G. (ed.) CP 2015. LNCS, vol. 9255, pp. 173–182. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23219-5_13
Jakl, M., Pichler, R., Rümmele, S., Woltran, S.: Fast counting with bounded treewidth. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 436–450. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89439-1_31
Janota, M., Marques-Silva, J.: On deciding MUS membership with QBF. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 414–428. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_32
Kloks, T. (ed.): Treewidth: Computations and Approximations. LNCS, vol. 842. Springer, Heidelberg (1994). https://doi.org/10.1007/BFb0045375
Lagniez, J.-M., Biere, A.: Factoring out assumptions to speed up MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 276–292. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_21
Lagniez, J.-M., Lonca, E., Mailly, J.-G.: CoQuiAAS: a constraint-based quick abstract argumentation solver. In: 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2015, pp. 928–935 (2015)
Lampis, M., Mitsou, V.: Treewidth with a quantifier alternation revisited (2017)
Langer, A., Reidl, F., Rossmanith, P., Sikdar, S.: Practical algorithms for MSO model-checking on tree-decomposable graphs. Comput. Sci. Rev. 13–14, 39–74 (2014)
Liberatore, P.: Redundancy in logic I: CNF propositional formulae. Artif. Intell. 163(2), 203–232 (2005)
Lifschitz, V.: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 3. Chapter Circumscription, pp. 297–352. Oxford University Press Inc., New York (1994)
Lokshtanov, D., Marx, D., Saurabh, S.: Lower bounds based on the exponential time hypothesis. Bull. EATCS 105, 41–72 (2011)
Marx, D., Mitsou, V.: Double-exponential and triple-exponential bounds for choosability problems parameterized by treewidth. In: 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, pp. 28:1–28:15 (2016)
McCarthy, J.: Applications of circumscription to formalizing common-sense knowledge. Artif. Intell. 28(1), 89–116 (1986)
Pan, G., Vardi, M.Y.: Fixed-parameter hierarchies inside PSPACE. In: 21st IEEE Symposium on Logic in Computer Science, LICS 2006, pp. 27–36 (2006)
Samer, M., Szeider, S.: Algorithms for propositional model counting. J. Discrete Algorithms 8(1), 50–64 (2010)
Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy: a compendium. SIGACT News 33(3), 32–49 (2002)
Marques-Silva, J., Lynce, I.: On improving MUS extraction algorithms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 159–173. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21581-0_14
Acknowledgments
Most of the research in this paper was performed during a stay of the first and third authors at CRIL that was financed by the project PEPS INS2I 2017 CODA. The second author is thankful for many valuable discussions with members of CRIL, in particular Jean-Marie Lagniez, Emmanuel Lonca and Pierre Marquis, on the topic of this article.
Moreover, the authors would like to thank the anonymous reviewers whose numerous helpful remarks allowed to improve the presentation of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Lampis, M., Mengel, S., Mitsou, V. (2018). QBF as an Alternative to Courcelle’s Theorem. In: Beyersdorff, O., Wintersteiger, C. (eds) Theory and Applications of Satisfiability Testing – SAT 2018. SAT 2018. Lecture Notes in Computer Science(), vol 10929. Springer, Cham. https://doi.org/10.1007/978-3-319-94144-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-94144-8_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-94143-1
Online ISBN: 978-3-319-94144-8
eBook Packages: Computer ScienceComputer Science (R0)