一句话：基于 ETH 证明按树宽和量词秩参数化的 QSat 需要 i 重指数时间，覆盖整个多项式谱系。
该论文研究量化布尔公式有效性（QSat）在参数化复杂性下的精细复杂度下界。已知结果：按原始图树宽与量词秩参数化，QSat 是固定参数可解的，运行时间为输入规模多项式、树宽 i 重指数，其中 i 为量词秩。论文追问在指数时间假设（ETH）下这一指数塔能否显著降低。作者对任意 QBF 建立了基于 ETH 的下界，证明对于量词秩 i 的 QSat，不存在运行时间显著优于树宽 i 重指数、输入规模多项式的算法，从而覆盖整个多项式谱系。技术方面，论文给出一种压缩树宽的归约技术，可在任意树分解上编码动态规划，并提出对多项式谱系更高层、按树宽参数化问题进行细粒度分析的一般方法。最后将结果应用于投影模型计数等更高层问题。
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.
DOI 原文 ·
@inproceedings{paperbot5509,
title = {Lower Bounds for QBFs of Bounded Treewidth},
author = {Johannes K. Fichte and Markus Hecher and Andreas Pfandler},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394756}
}