Title: Small Resolution Proofs for QBF using Dependency Treewidth,
Abstract: In spite of the close connection between the evaluation of quantified Boolean
formulas (QBF) and propositional satisfiability (SAT), tools and techniques
which exploit structural properties of SAT instances are known to fail for QBF.
This is especially true for the structural parameter treewidth, which has
allowed the design of successful algorithms for SAT but cannot be
straightforwardly applied to QBF since it does not take into account the
interdependencies between quantified variables.
In this work we introduce and develop dependency treewidth, a new structural
parameter based on treewidth which allows the efficient solution of QBF
instances. Dependency treewidth pushes the frontiers of tractability for QBF by
overcoming the limitations of previously introduced variants of treewidth for
QBF. We augment our results by developing algorithms for computing the
decompositions that are required to use the parameter.