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.

• Type: Conference
• Year: 2004
• Where: BIRTHDAY
• Authors: Hans Kleine Büning, Xishun Zhao
• Keywords: Applied Computing, BIRTHDAY 2004, Boolean Functions, Boolean Horn Formula, Quantified Boolean Formulas