Backdoors for Quantified Boolean Formulas

Abstract

The quantified Boolean formula problem (QBF) is a well-known PSpace-complete problem with rich expressive power, and is generally viewed as the SAT analogue for PSpace. Given that many problems today are solved in practice by reducing to SAT, and then using highly optimized SAT solvers, it is natural to ask whether problems in PSpace are amenable to this approach. While SAT solvers exploit hidden structural properties, such as backdoors to tractability, backdoor analysis for QBF is comparatively very limited. We present a comprehensive study of the (parameterized) complexity of QBF parameterized by backdoor size to the largest tractable syntactic classes: HORN, 2-SAT, and AFFINE. While SAT is in FPT under this parameterization, we prove that QBF remains PSpace-hard even on formulas with backdoors of constant size. Parameterizing additionally by the quantifier depth, we design FPT-algorithms for the classes 2-SAT and AFFINE, and show that 3-HORN is W[1]-hard. As our next contribution, we vastly extend the applicability of QBF backdoors not only for the syntactic classes defined above but also for tractable classes defined via structural restrictions, such as formulas with bounded incidence treewidth and quantifier depth. To this end, we introduce enhanced backdoors: these are separators S of size at most k in the primal graph such that S together with all variables contained in any purely universal component of the primal graph minus S is a backdoor. We design FPT-algorithms with respect to k for both evaluation and detection of enhanced backdoors to all tractable classes of QBF listed above and more.