Fixed-Parameter Tractability of Dependency QBF with Structural Parameters

Abstract

We studydependency quantified Boolean formulas(DQBF),an extension of QBF in which dependencies of existentialvariables are listed explicitly rather than being implicit inthe order of quantifiers. DQBF evaluation is a canonicalNEXPTIME-complete problem, a complexity class contain-ing many prominent problems that arise in Knowledge Rep-resentation and Reasoning.One approach for solving such hard problems is to identifyand exploit structural properties captured by numerical pa-rameters such that bounding these parameters gives rise toan efficient algorithm. This idea is captured by the notionof fixed-parameter tractability (FPT). We initiate the studyof DQBF through the lens of fixed-parameter tractabilityand show that the evaluation problem becomes FPT undertwo natural parameterizations: the treewidth of the primalgraph of the DQBF instance combined with a restriction onthe interactions between the dependency sets, and also thetreedepth of the primal graph augmented by edges represent-ing dependency sets.