Backdoor Sets of Quantified Boolean FormulasJournal of Automated Reasoning, vol. 42, no. 1, pp. 77-97, 2009. A preliminary and shortened version appeared in the Proceedings of SAT 2007, Tenth International Conference on Theory and Applications of Satisfiability Testing, May 28-31, 2007, Lisbon, Portugal, Lecture Notes in Computer Science, vol. 4501, pp. 230-243, 2007. Abstract:We generalize the notion of backdoor sets from propositional formulas to quantified Boolean formulas (QBF). This allows us to obtain hierarchies of tractable classes of quantified Boolean formulas with the classes of quantified Horn and quantified 2CNF formulas, respectively, at their first level, thus gradually generalizing these two important tractable classes. In contrast to known tractable classes based on bounded treewidth, the number of quantifier alternations of our classes is unbounded. As a side product of our considerations we develop a theory of variable dependency which is of independent interest.Download: [paper pdf] |