2006 | OriginalPaper | Buchkapitel
Dependency Quantified Horn Formulas: Models and Complexity
verfasst von : Uwe Bubeck, Hans Kleine Büning
Erschienen in: Theory and Applications of Satisfiability Testing - SAT 2006
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.