Backdoor Sets of Quantified Boolean Formulas

Backdoor Sets of Quantified Boolean Formulas
复制标题

DOI:
10.1007/s10817-008-9114-5
复制
发表时间:
2009-01-01
期刊:
JOURNAL OF AUTOMATED REASONING
影响因子:
--
通讯作者:
Szeider, Stefan
Szeider, Stefan
中科院分区:
其他
文献类型:
--
作者:
Samer, Marko;Szeider, Stefan

文献摘要

被引文献

相似文献

我们将后门集的概念从命题公式推广到量化布尔公式(QBF)。这使我们能够获得层次结构的易于处理的类的量化布尔公式与类的量化霍恩和量化2CNF公式,分别在其第一级,从而逐步推广这两个重要的易于处理的类。与已知的基于有界树宽的易处理类相比,我们的类的量词交替的数量是无界的。作为我们的考虑的副产品,我们开发了一个理论的变量依赖,这是独立的利益。
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.