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 phi of length vertical bar phi vertical bar with free variables, vertical bar for all vertical bar universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent quantified Horn formula of length O(vertical bar for all vertical bar . vertical bar phi vertical bar) 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(vertical bar for all vertical bar . vertical bar phi vertical bar) 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. (C) 2007 Elsevier B.V. All rights reserved.