QBF as an Alternative to Courcelle's Theorem

Authors: Michael Lampis, Stefan Mengel and Valia Mitsou

Paper Information

Title:QBF as an Alternative to Courcelle's Theorem
Authors:Michael Lampis, Stefan Mengel and Valia Mitsou
Proceedings:SAT Proceedings
Editors: Christoph M. Wintersteiger and Olaf Beyersdorff
Keywords:QBF, parameterized complexity, treewidth, artificial intelligence

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 in 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. 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.

Talk:Jul 10 16:00 (Session 58C: QBF II)