2006 | OriginalPaper | Chapter
Dependency Quantified Horn Formulas: Models and Complexity
Authors : Uwe Bubeck, Hans Kleine Büning
Published in: Theory and Applications of Satisfiability Testing - SAT 2006
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.