Models and quantifier elimination for quantified Horn formulas

In this paper, quantified Horn formulas (QHORN) are investigated. We prove that the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. Accordingly, we give a detailed characterization of QHORN satisfiability models which describe the set of satisfying truth assignments to the existential variables. We also consider quantified Horn formulas with free variables (QHORN^*) and show that they have monotone equivalence models.The main application of these findings is that any quantified Horn formula Φ of length |Φ| with free variables, |∀| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent quantified Horn formula of length O(|∀|·|Φ|) which contains only existential quantifiers.We also obtain a new algorithm for solving the satisfiability problem for quantified Horn formulas with or without free variables in time O(|∀|·|Φ|) by transforming the input formula into a satisfiability-equivalent propositional formula. Moreover, we show that QHORN satisfiability models can be found with the same complexity.