Backdoor Sets of Quantified Boolean Formulas |
| |
Authors: | Marko Samer Stefan Szeider |
| |
Affiliation: | (1) TU Darmstadt, Darmstadt, Germany;(2) University of Durham, Durham, UK |
| |
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. |
| |
Keywords: | Quantified Boolean formulas Backdoor sets Variable dependencies Parameterized complexity |
本文献已被 SpringerLink 等数据库收录! |
|