Solving Quantified Boolean Formulas and its Applications

Speaker: Martina Seidel, Johannes Kepler University, Linz, Austria

Tuesday Feb 20 2024, 14:00, Room 1Z53

Abstract: Quantified Boolean Formulas (QBFs) extend propositional logic by quantifiers over the Boolean variables. Despite the PSPACE hardness of their decision problem, much progress has been made in practical solving, making QBFs an attractive framework for encoding various problems from artificial intelligence and formal verification.

In this talk, we will give an overview on recent trends and developments in QBF solving and we will discuss promising applications of QBFs.