Quantified Boolean Formulae Project Home Page

• Goal:
  • Design and implementation of efficient algorithms for evaluating Quantified Boolean Formulae.
  • Translation of various problems in the PSPACE complexity class into QBF evaluation.
  • Understanding which are the hard cases for QBF evaluation.
• People involved:
  • Marco Cadoli
  • Massimo Giovanardi
  • Marco Schaerf
  
  
• Code
  • QBF generation
    • Readme file
    • Solaris 2.5 executable (gzipped file)
    • Example of a generated QBF ( meaning)
  • Evaluation of a QBF
    • Readme file
    • Solaris 2.5 executable (gzipped file)
    • Example of the evaluation of a QBF
  • Translations between various QBF formats
    • From Rintanen's format to our format
      • Example of a formula in Rintanen's format
      • Solaris 2.5 executable (gzipped file)
    • From our format to Lettmann's format
      • Explanation of Lettmann's format
      • Readme file
      • Solaris 2.5 executable (gzipped file)
      • Previous example translated in Lettmann's format
  
  
• Papers
  • An Algorithm to Evaluate Quantified Boolean Formulae. by M. Cadoli, A. Giovanardi, M. Schaerf .
    Proc. of AAAI-98, July, 1998. Download a gzipped postscript version of the paper
  • Experimental Analysis of the Computational Cost of Evaluating Quantified Boolean Formulae. by M. Cadoli, A. Giovanardi, M. Schaerf.
    Proc. of AI*IA-97, Springer LNAI, 1997.
    Download a gzipped postscript version of the paper
  • An Algorithm to Evaluate Quantified Boolean Formulae and its Experimental Evaluation. by M. Cadoli, M. Schaerf, A. Giovanardi, M. Giovanardi.
    Technical report DIS 08-99, March 1999. Significantly extended version of AI*IA-97 and AAAI-98.
    Download a gzipped postscript version of the paper.
    Revised version as of June 10, 1999.

Other people working on QBFs

• Jussi Rintanen
• Theodor Lettmann
• www.qbflib.org page

---

Back to Marco Cadoli's Home Page.

---

(Last update )