News
Currently, no news are available
Quantified Boolean Formulas: Algorithms and Applications
Overview
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.
Audience
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).
Structure
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
- ...