Subclasses of quantified boolean formulas

  • Andreas Flögel
  • Marek Karpinski
  • Hans Kleine Büning
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 533)


Using the results of a former paper of two of the authors [KaKB 90], for certain subclasses of quantified Boolean formulas it is shown, that the evaluation problems for these classes are coNP-complete. These subclasses can be seen as extensions of Horn and 2-CNF formulas.

Further it is shown that the evaluation problem for quantified CNF formulas remains PSPACE-complete, even if at most one universal variable is allowed in each clause.


Evaluation Problem Boolean Formula Propositional Formula Unit Clause Universal Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AaBo 79]
    S. O. Aanderaa, E. Börger: The Horn complexity of Boolean functions and Cook's problem, Proc. 5th Scand.Logic Symp. (Eds.B.Mayoh, F.Jensen), 1979, 231–256Google Scholar
  2. [APT 78]
    B. Aspvall, M. F. Plass and R.E. Tarjan: A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas, Information Processing Letters, Volume 8, number 3, 1978, 121–123CrossRefGoogle Scholar
  3. [DoGa 84]
    W. F. Dowling and J. H. Gallier: Linear-Time Algorithms For Testing The Satisfiability Of Propositional Horn Formulae, J. of Logic Programming, 1984, 267–284Google Scholar
  4. [GJ 79]
    M. R. Garey and D. S: Johnson: Computers and Intractability, A Guide to the Theory of NP-Completeness, W. H. Freemann and Co., New York, 1979Google Scholar
  5. [Ha 85]
    A. Haken: The intractability of resolution, Theoret. Comput. Sci. 39, 1985, 297–308CrossRefGoogle Scholar
  6. [KaKB 90]
    M.Karpinski, H.Kleine Büning: Resolution for Quantified Boolean Formulas, submitted for publicationGoogle Scholar
  7. [KKBS 87]
    M. Karpinski, H. Kleine Büning and P.H. Schmitt: On the computational complexity of quantified Horn clauses, Lecture Notes in Computer Science 329, Springer-Verlag, 1987, 129–137Google Scholar
  8. [StM 73]
    L. J. Stockmeyer and A. R. Meyer: Word problems requiring exponential time, Proc. 5th Ann. ACM Symp. Theory of Computing, 1973, 1–9Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Andreas Flögel
    • 1
  • Marek Karpinski
    • 2
  • Hans Kleine Büning
    • 1
  1. 1.FB 11-Praktische InformatikUniversität DuisburgDuisburg 1Germany
  2. 2.Institut für InformatikUniversität BonnBonnGermany

Personalised recommendations