Invited Talk, Thursday, April 20, 2023, Technische Fakultät, Geb. 101, SR 2-16/18
Beyond NP: Reasoning with Quantified Boolean Formulas
Prof. Dr. Martina Seidl
Institute for Symbolic Artificial Intelligence
Johannes Kepler University Linz, Austria
Abstract
As the prototypical NP-complete problem SAT, the decision problem of propositional logic, is considered to be hard. Despite this hardness, SAT is very successfully applied in many practical domains, because very powerful reasoning techniques are available. There are, however, problems that cannot be efficiently encoded in SAT. For such problems, formalisms with decision problems beyond NP are necessary. One of such formalisms are quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers over the Boolean variables. The QBF decision problem is PSPACE-complete, making QBF well suitable for encoding and solving many problems from formal verification, synthesis, and artificial intelligence. In this talk, we give a short tour through recent developments in QBF solving.