Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges
A tutorial presented at the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), New York City, USA
Solving (Problems with) Quantified Boolean Formulas: Recent Trends and Challenges
A tutorial presented at the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), New York City, USA
Image credits: Pixabay, Creative Commons CC0
The logic of quantified Boolean formulas (QBF) extends propositional logic by explicit existential or universal quantification of propositional variables. The problem to check whether a given QBF is satisfiable is PSPACE-complete, which is in contrast to the NP-completeness of the satisfiability problem of propositional logic (SAT). QBFs are a natural formalism to encode problems from the complexity class PSPACE or from subclasses in the polynomial hierarchy. Related examples are planning, abstract argumentation, answer set programming, or the computation of smallest unsatisfiable subformulas. Due to explicit quantifiers, QBF encodings of problems are potentially exponentially more succinct than encodings in propositional logic. Hence QBF is an important modeling language to encode and solve problems in practice.
This tutorial presents QBFs from a theoretical and practical perspective. It introduces and reviews the state of the art in QBF research and aims at providing non-specialists with the necessary background to apply QBF-based techniques in practice. The tutorial targets both practitioners and theoreticians who would like to apply QBF-related techniques to solve a particular problem by modelling it as a QBF, or who aim at transferring ideas which were found successful in the QBF domain to other problem domains.
Presentation slides (minor fixes July 25, 2016): PDF
| Florian Lonsing |  |
| Knowledge-Based Systems Group | |
| Institute of Information Systems | |
| Vienna University of Technology, Austria | |
| http://www.kr.tuwien.ac.at/staff/lonsing/ |
Florian Lonsing is a post-doctoral researcher in the Knowledge-Based Systems Group (KBS) at Vienna University of Technology, Austria, which he joined in 2012. His position is part of the Austrian-wide RiSE/SHiNE research project funded by the Austrian Science Fund (FWF). Florian Lonsing studied computer science at Johannes Kepler University (JKU), Linz, Austria (PhD 2012) and was a research and teaching assistant at the Institute for Formal Models and Verification at JKU from 2008 to 2012. His current research activities focus on decision procedures for quantified Boolean formulas (QBF) and related theoretical and practical aspects, e.g., approaches to automated testing and debugging of solvers, incremental solving, and experimental evaluation. He has been developing the state of the art QBF solver DepQBF, which achieved top rankings in several QBF solver competitions.
This work is supported by the Austrian Science Fund (FWF) under grant S11409-N23.