On boolean models for quantified boolean horn formulas

Abstract

For a Quantified Boolean Formula (QBF) Φ = Qφ, an assignment is a function ℳ. that maps each existentially quantified variable of Φ to a Boolean function, where φ is a propositional formula and Q is a linear ordering of quantifiers on the variables of Φ. An assignment ℳ. is said to be proper, if for each existentially quantified variable yi the associated Boolean function fi does not depend upon the universally quantified variables whose quantifiers in Q succeed the quantifier of y i. An assignment ℳ is said to be a model for Φ, if it is proper and the formula φℳ is a tautology, where φℳ is the formula obtained from φ by substituting f i for each existentially quantified variable yi. We show that any true quantified Horn formula has a Boolean model consisting of monotone monomials and constant functions only; conversely, if a QBF has such a model then it contains a clause-subformula in QHORN ∩ SAT. © Springer-Verlag 2004.