[Back]

J. Fichte, M. Hecher, A. Pfandler:
"Lower Bounds for QBFs of Bounded Treewidth";
Talk: LICS 2020, Saarbrücken, Germany; 2020-07-08 - 2020-07-11; in: "LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020", (2020), 410 - 424.

The problem of deciding the validity (QSat) of quantified
Boolean formulas (QBF) is a vivid research area in both theory
and practice. In the field of parameterized algorithmics,
the well-studied graph measure treewidth turned out to be
a successful parameter. A well-known result by Chen [9]
is that QSat when parameterized by the treewidth of the
primal graph and the quantifier rank of the input formula
is fixed-parameter tractable. More precisely, the runtime of
such an algorithm is polynomial in the formula size and exponential
in the treewidth, where the exponential function
in the treewidth is a tower, whose height is the quantifier
rank. A natural question is whether one can significantly
improve these results and decrease the tower while assuming
the Exponential Time Hypothesis (ETH). In the last years,
there has been a growing interest in the quest of establishing
lower bounds under ETH, showing mostly problem-specific
lower bounds up to the third level of the polynomial hierarchy.
Still, an important question is to settle this as general
as possible and to cover the whole polynomial hierarchy.
In this work, we show lower bounds based on the ETH for
arbitrary QBFs parameterized by treewidth and quantifier
rank. More formally, we establish lower bounds for QSat
and treewidth, namely, that under ETH there cannot be an
algorithm that solves QSat of quantifier rank i in runtime
significantly better than i-fold exponential in the treewidth
and polynomial in the input size. In doing so, we provide
a reduction technique to compress treewidth that encodes
dynamic programming on arbitrary tree decompositions.
Further, we describe a general methodology for a more finegrained
analysis of problems parameterized by treewidth
that are at higher levels of the polynomial hierarchy. Finally,
we illustrate the usefulness of our results by discussing various
applications of our results to problems that are located
higher on the polynomial hierarchy, in particular, various
problems from the literature such as projected model counting
problems.

Parameterized Complexity, ETH, Lower Bounds, Quantified Boolean Formulas, Treewidth, Pathwidth

http://dx.doi.org/10.1145/3373718.3394756

Project Head Stefan Woltran:
START