QBF as an Alternative to Courcelle’s Theorem
Lampis, Michael; Mengel, Stefan; Mitsou, Valia (2018), QBF as an Alternative to Courcelle’s Theorem, in Olaf Beyersdorff; Christoph M. Wintersteiger, Theory and Applications of Satisfiability Testing – SAT 2018, 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings, Springer International Publishing : Berlin, p. 235-252. 10.1007/978-3-319-94144-8_15
TypeCommunication / Conférence
External document linkhttps://arxiv.org/abs/1805.08456v1
Conference title21st International Conference on Theory and Applications of Satisfiability Testing – SAT 2018
Conference countryUnited Kingdom
Book titleTheory and Applications of Satisfiability Testing – SAT 2018, 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings
Book authorOlaf Beyersdorff; Christoph M. Wintersteiger
MetadataShow full item record
Laboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
Centre de Recherche en Informatique de Lens [CRIL]
Institut de Recherche en Informatique Fondamentale [IRIF (UMR_8243)]
Abstract (EN)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.
Subjects / Keywordsquantified Boolean formulas
Showing items related by title and author.