Bilateral Treewidth for QBF: Where Strategies and Resolution Meet

TL;DR

This paper introduces bilateral treewidth, a new parameter that combines strategy and resolution techniques, enabling fixed-parameter tractability for evaluating QBFs, which was previously unresolved.

Contribution

The paper proposes bilateral treewidth, a novel parameter that unifies strategy and resolution approaches, establishing fixed-parameter tractability for QBF evaluation.

Findings

Bilateral treewidth is strictly more powerful than previous variants.

The authors' algorithm is fixed-parameter tractable given a suitable tree decomposition.

This approach unifies previously separate methods for QBF evaluation.

Abstract

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.