Advanced Topics in Informatics

Reasoning Techniques for Quantified Boolean Formulas

Spezielle Kapitel in Informatik (3KV)

Summer Semester 2012

Course has been cancelled due to too few participants. If you are interested in the topic, please contact Martina Seidl.


Dr. Martina Seidl


Quantified Boolean formulas (QBF) find their application in several domains of formal verification and artificial intelligence like planning, model checking, etc. QBF extend propositional logic with quantifiers over the variables raising the complexity of the decision problem from NP to PSPACE.

In this course, an overview of the state-of-the-art QBF solving is given and in small groups (2-3 students), the participants will implement reasoning techniques for QBF.

Four lectures at the beginning of the semester will provide the necessary basics on quantified Boolean formulas. During the semester, meetings with the supervisor are scheduled individually for progress reporting and feedback. At the end of the semester, the results have to be presented to all participants of the course.

The attendance of the lecture Advanced Model Checking is recommended.

Schedule (tentative)

The lectures are from 15:30-17:00 in T038/1.
  • 13.03.2012: Administrative issues; first lecture