Reasoning Techniques for Quantified Boolean Formulas

Overview

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)

• 13.03.2012: Administrative issues; first lecture

Resources