On Models for Quantified Boolean Formulas

13 years 11 months ago
On Models for Quantified Boolean Formulas
A quantified Boolean formula is true, if for any existentially quantified variable there exists a Boolean function depending on the preceding universal variables, such that substituting the existential variables by the Boolean functions results in a true formula. We call a satisfying set of Boolean functions a model. In this paper, we investigate for various classes of quantified Boolean formulas and various classes of Boolean functions the problem whether a model exists. Furthermore, for these classes the complexity of the model checking problem - whether a set of Boolean functions is a model for a formula - will be shown. Finally, for classes of Boolean functions we establish some characterizations in terms of quantified Boolean formulas which have such a model. For example, roughly speaking any satisfiable quantified Boolean Horn formula can be satisfied by monomials and vice versa.
Hans Kleine Büning, Xishun Zhao
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Authors Hans Kleine Büning, Xishun Zhao
Comments (0)