Treewidth is a well-studied decompositional parameter to measure the tree-likeness of a graph. While the propositional satisfiability problem (SAT) is known to be tractable when parameterized by the treewidth of the underlying primal graph, the evaluation of quantified Boolean formulas (QBFs) remains PSPACE-complete even on formulas of constant treewidth. Intuitively, this is because ordinary treewidth does not take into account the prefix of the QBF: it neither distinguishes between existential and universal variables, nor accounts for the order in which they are quantified. In the past, several weaker variants of treewidth have been devised to incorporate prefix-sensitive information. To establish tractability for QBFs under these notions, prior work has employed either strategy- or resolution-based techniques, thereby dividing the parameterized complexity landscape of QBF into two regimes that are incomparable in strength. We establish fixed-parameter tractability with respect to bilateral treewidth, a novel and strictly more powerful decompositional parameter that combines these rivaling approaches by simultaneously allowing for branching on strategies and performing Q-resolution. As in previous works in this direction, our algorithm assumes that a suitable tree decomposition is provided on the input.

翻译：树宽是衡量图树状结构的一个经过充分研究的分解参数。虽然命题可满足性问题（SAT）在底层原始图的树宽参数化下是易解的，但量化布尔公式（QBF）的求值即使在恒定树宽的公式上仍然是PSPACE完全的。直观地说，这是因为普通树宽未考虑QBF的前缀：它既未区分存在变量与全称变量，也未考虑它们的量化顺序。过去，研究者设计了几种较弱的树宽变体以纳入前缀敏感信息。为了在这些概念下建立QBF的可解性，先前的工作采用了基于策略或基于消解的技术，从而将QBF的参数化复杂度分为两个强度不可比较的领域。我们建立了关于双边树宽的固定参数可解性——这是一种新颖且严格更强的分解参数，通过允许同时对策略进行分支和执行Q-消解，将这两种相互竞争的方法结合起来。与这一方向的先前工作一致，我们的算法假设输入中提供了合适的树分解。