Backdoor Sets of Quantified Boolean Formulas
Backdoor Sets of Quantified Boolean Formulas
复制标题
DOI:
10.1007/s10817-008-9114-5
复制
发表时间:
2009-01-01
期刊:
影响因子:
--
通讯作者:
Szeider, Stefan
中科院分区:
文献类型:
--
作者:
Samer, Marko;Szeider, Stefan
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.