ABSTRACT. We give an overview of the main paradigms in QBF solving, as well as techniques for preprocessing. In each case, we present corresponding proof systems and discuss lower bound results. We point to open problems, and consider current trends in solver development.

ABSTRACT. Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of the QCDCL models are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.

ABSTRACT. We give an overview of the main paradigms in QBF solving, as well as techniques for preprocessing. In each case, we present corresponding proof systems and discuss lower bound results. We point to open problems, and consider current trends in solver development.

ABSTRACT. Invited talk.

ABSTRACT. Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of the QCDCL models are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL. This is a continuation of a previous talk with the same title. While in the previous talk we focused on the general techniques of showing QCDCL lower bounds, here we focus on the specifics pertaining to pure literal elimination and cube learning.

ABSTRACT. Augmenting problem variables in a quantified Boolean formula with definition variables enables a compact representation in clausal form. Generally these definition variables are placed in the innermost quantifier level. To restore some structural information, we introduced a preprocessing technique that moves definition variables to the quantifier level closest to the variables that define them. We express the movement in the QRAT proof system to allow verification by independent proof checkers. We evaluated definition variable movement on the QBFEVAL'20 competition benchmarks. Movement significantly improved performance for the competition's top solvers. Combining variable movement with the preprocessor bloqqer improves solver performance compared to using bloqqer alone.

This work appeared in a TACAS'22 paper under the same title.

ABSTRACT. Quantified Integer Programs (QIP) are integer linear programs where variables are either existentially or universally quantified. Similar to the link from SAT to Integer Programming, a connection between QBF and QIP can be drawn: QIP extends QBF by allowing general integer variables and linear constraints in addition to a linear objective function. We review solution methods, recent developments, and extensions in order to display future research directions and opportunities.

ABSTRACT. Given a relational specification between Boolean inputs and outputs, the problem of Boolean functional synthesis is to construct each output as a function of the inputs such that the specification is met. Synthesizing Boolean functions is one of the challenging problems in Computer Science. Over the decades, the problem has found applications in a wide variety of domains such as certified QBF solving, automated program repair, program synthesis, and cryptography.

In this talk, we will discuss Manthan, a novel data-driven approach for Boolean functional synthesis. Manthan views the problem of functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification.

ABSTRACT. The Dynamic Logic of Propositional Assignments (DL-PA) is a formalism that combines logic, programming, and non-determinism constructs. Starting with DL-PA, we build reductions to and from Quantified Boolean Formulas. This prompts us to unexpectedly revisit prenexing and clausification procedures for quantified propositional formulas. To the best of our knowledge, this latter task was not completly settled when the equivalence operator is involved. (Joint work with Andreas Herzig.)

ABSTRACT. The problem of deciding the validity (QSat) of quantified Boolean formulas (QBF) is a vivid research area in both theory and practice. In the field of parameterized algorithmics, the well-studied graph measure treewidth turned out to be a successful parameter. A well-known result by Chen [9] is that QSat when parameterized by the treewidth of the primal graph and the quantifier rank of the input formula is fixed-parameter tractable. More precisely, the runtime of such an algorithm is polynomial in the formula size and exponential in the treewidth, where the exponential function in the treewidth is a tower, whose height is the quantifier rank. A natural question is whether one can significantly improve these results and decrease the tower while assuming the Exponential Time Hypothesis (ETH). In the last years, there has been a growing interest in the quest of establishing lower bounds under ETH, showing mostly problem-specific lower bounds up to the third level of the polynomial hierarchy. Still, an important question is to settle this as general as possible and to cover the whole polynomial hierarchy. In this work, we show lower bounds based on the ETH for arbitrary QBFs parameterized by treewidth and quantifier rank. More formally, we establish lower bounds for QSat and treewidth, namely, that under ETH there cannot be an algorithm that solves QSat of quantifier rank i in runtime significantly better than i-fold exponential in the treewidth and polynomial in the input size. In doing so, we provide a reduction technique to compress treewidth that encodes dynamic programming on arbitrary tree decompositions. Further, we describe a general methodology for a more finegrained analysis of problems parameterized by treewidth that are at higher levels of the polynomial hierarchy. Finally, we illustrate the usefulness of our results by discussing various applications of our results to problems that are located higher on the polynomial hierarchy, in particular, various problems from the literature such as projected model counting problems.