Quantified Boolean Formulas: Proof Complexity and Solving

• Applicant: Professor Dr. Olaf Beyersdorff
• Subject Area: Theoretical Computer Science
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 462332910

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 QBF solving, which are amenable to a complexity analysis, thereby identifying both limitations of current solving paradigms and new directions for algorithmic improvement. The focal point of our analysis is QBF, which in comparison to SAT presents an algorithmically even more challenging problem and reaches out to more applications.Methodologically, our main approach is 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, large classes of families of hard formulas, and proof search heuristics.In its first project phase we already laid the ground with a solid theoretical modelling and proof-complexity analysis of classic QCDCL, one of the main contemporary solving approaches in QBF, generalising the successful CDCL paradigm of SAT solving. We devised a new lower bound technique tailored for QCDCL and established the relations of QCDCL to major QBF proof systems. The second project phase will build on this ground and advance our analysis from standard QCDCL to state-of-the-art solving methods including dependency learning and schemes. This requires significantly stronger techniques and new classes of QBFs. In parallel, we will start the transitioning of our theoretical findings into practice by devising decision and reduction heuristics for strong solving models and provide proof-of-concept implementations.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.

• DFG Programme: Research Grants
• International Connection: Austria, India, Spain
• Cooperation Partners: Professor Ilario Bonacina; Professorin Meena Mahajan; Dr. Tomas Peitl