Quantified Boolean Formulas: Algorithms and Applications Ralf Wimmer



Keine Sprechstunde am 18.11.2015

Liebe Teilnehmer am QBF-Seminar,

da ich am 18.11. wichtige Termine in Freiburg habe, muss die Sprechstunde an diesem Tag leider ausfallen.

Viele Grüße

   Ralf Wimmer.



Quantified Boolean Formulas: Algorithms and Applications


In this seminar we will study quantified Boolean formulas (QBFs) and their generalization to dependency quantified Boolean formulas (DQBFs). During the last decade, tools have been developed which allow to solve QBFs with thousands of variables and clauses efficiently. This makes it possible to use QBF formulations in various practically relevant applications, ranging from the verification of digital systems over the synthesis of safe controllers to planning problems from artificial intelligence.


This seminar addresses Bachelor and Master students from computer science

Number of participants

The seminar is limited to 12 students.

First meeting

The first meeting will be on Wednesday, October 21, 2015 at 14:15 in Building E1 3, Room 528 (5th floor).


Each student will be assigned one topic from QBF/DQBF solving, consisting of 1-3 papers. The student's tasks are

  • to prepare a talk of 45 min on the assigned topic and present it to the other students/advisors
  • to attend the talks of the other students and actively participate in the discussion
  • to write a handout of 10-15 pages on the assigned topic

List of topics

  • Foundations of QBF: Theory
  • Foundations of QBF: Search-based Solving
  • Foundations of DQBF: Theory and Elimination-based Solving
  • Preprocessing for QBF/DQBF
  • Dependency Schemes for QBF
  • Certification for QBF
  • CEGAR-based solution of QBFs
  • Instantiation-based solution of DQBFs
  • QBF and DQBF for the Verification of Incomplete Circuits
  • ...


If you encounter technical problems, please contact the administrators