Quantifizierte Boolesche Formeln: Beweiskomplexität und Solving

Duration: 2021-2024
funded by the German Research Foundation (DFG)

Scientific goals:
The satisfiability problems for propositional logic (SAT) and for quantified Boolean formulas (QBF) are central computational problems within theoretical computer science: a vibrant field with the two main facets of algorithms and complexity. From a complexity perspective, SAT and QBF are hard problems as they are NP- and even PSPACE-complete. This sharply contrasts with their modern algorithmic treatment by SAT and QBF solvers, which routinely solve huge industrial instances and provide ubiquitous tools for tackling hard computational problems from almost all application domains.

This project aims to create a theory of SAT and QBF solving that explains and assesses this success of solving. The central objective of this proposal is to build concise theoretical models of SAT and QBF solving, which are amenable to a complexity analysis, thereby identifying both limitations of current solving paradigms and new directions for improvement. The focal point of our analysis will be QBF, which in comparison to SAT presents an algorithmically even more challenging problem and reaches out to more applications.

Methodologically, our main approach will be through proof complexity. While each solver implicitly defines a logical proof system, the challenge is to create lean proof-theoretic models of actual solving. To analyse these models, we will advance the field of QBF proof complexity through new lower bound techniques, new families of hard formulas, and proof search.

This theoretical project has the potential for massive impact, both in solving and in proof complexity. New theoretical models could lead to better SAT/QBF solvers. This is a timely opportunity for QBF: while some of the main breakthroughs in SAT took place in the late 1990s, QBF solving is currently undergoing a period of exciting algorithmic innovation. For proof complexity, our project will present a step change from abstract logical calculi towards models of actual solving, thus helping to narrow the widely lamented theory-practice gap between proof complexity and solving.