Dependency Quantified Horn Formulas: Models and Complexity
Dependency Quantified Horn Formulas: Models and Complexity
复制标题
依赖性量化喇叭公式：模型和复杂性
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
H. K. Büning
中科院分区：
文献类型：
--
作者：
Uwe Bubeck;H. K. Büning
依赖量化布尔公式（DQBF）是对量化布尔公式的扩展，它采用henkin式偏序量词。已经证明，这可能产生更简洁的表示，但代价是从PSPACE到NEXPTIME的计算量激增。本文考虑了依赖量化Horn公式（DQHORN），它是DQBF的一个子类，并证明了当添加部分有序量词时，量化Horn公式的计算简单性得以保持。
Dependency quantified Boolean formulas (DQBF) extend quantified Boolean formulas with Henkin-style partially ordered quantifiers. It has been shown that this is likely to yield more succinct representations at the price of a computational blow-up from PSPACE to NEXPTIME. In this paper, we consider dependency quantified Horn formulas (DQHORN), a subclass of DQBF, and show that the computational simplicity of quantified Horn formulas is preserved when adding partially ordered quantifiers.
We investigate the structure of satisfiability models for DQHORN formulas and prove that for both DQHORN and ordinary QHORN formulas, the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. This allows us to transform DQHORN formulas with free variables into equivalent QHORN formulas with only a quadratic increase in length.
An application of these findings is to determine the satisfiability of a dependency quantified Horn formula Φ with |∀| universal quantifiers in time O(|∀|·|Φ|), which is just as hard as QHORN-SAT.