Backdoor Sets of Quantified Boolean Formulas (bibtex)

by Marko Samer, Stefan Szeider

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.

Reference:

Backdoor Sets of Quantified Boolean FormulasMarko Samer, Stefan SzeiderJournal of Automated Reasoning (JAR), volume 42, number 1, pages 77–97, January 2009.

Bibtex Entry:

@article{SamSze09JAR, author = {Marko Samer and Stefan Szeider}, title = {Backdoor Sets of Quantified Boolean Formulas}, number = {1}, month = {January}, year = {2009}, journal = {Journal of Automated Reasoning (JAR)}, pages = {77--97}, volume = {42}, 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.}, issn = {0168-7433}, doi = {10.1007/s10817-008-9114-5} }

Powered by bibtexbrowser