The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.

翻译：量化布尔公式（QBF）问题是一个重要的判定问题，通常被视为PSPACE完全性的原型。人工智能领域许多核心问题（如规划、模型检测和非单调推理）通常不包含在NP中，而QBF已被成功用作这些问题的建模工具。然而，QBF求解器的成熟度远不及最先进的SAT求解器，这阻碍了QBF成为PSPACE完全问题的通用建模语言。理论解释在于QBF（以及许多其他PSPACE完全问题）缺乏保证固定参数可解性（FPT）的自然参数。本文针对该问题，考虑了一个简单但被忽视的参数：存在量词变量的数量。这一自然参数在文献中几乎未被探索，考虑到QBF的FPT算法普遍稀缺，这一现象令人惊讶。通过这一参数化，我们开发了一种新颖的FPT算法，适用于子句长度有界且处于合取范式（CNF）的QBF实例。作为补充，我们给出了子句长度无界的CNF-QBF的W[1]-难结果，以及在（强）指数时间假设下，对有界元数情形的更紧下界。