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 prepositional 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 y_i, the associated Boolean function f_i does not depend upon the universally quantified variables whose quantifiers in Q succeed the quantifier of y_i. An assignment M 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 y,. 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.
展开▼
