From QBF to DQBF: Theory together with Practice

Mathematical and computerized optimization is by now an essential ingredient of both private and industrial life. Unfortunately, as it turns out optimization is typically really hard. In fact, it is sometimes so hard that already finding any solution of some problem---the search version of the problem---is infeasible, not to mention finding the optimal one. Consider for instance the travelling salesperson problem, where we are interested in the shortest route that visits each of a set of destinations. Already deciding whether there is any route that visits each destination in under a given total time is hard. In spite of this inherent hardness, scientists have developed algorithms and software that can solve large, practically relevant optimization/search problems. But since it would be impractical and costly to develop software for every single application from scratch, we instead have a handful of solvers for the most general problems, and we encode other problems in their languages. Unfortunately, hardness strikes again. As it turns out, it is not only hard to solve problems, sometimes it is hard even to translate them to a different language. More expressive languages are needed in order to encode problems of higher complexity. Here is where quantification comes in. Consider the problem of finding the optimal strategy for chess. We can encode the strategy into the following formula: there is a move of White, such that for all moves of Black, there is a move of White, ..., such that White mates. Alternation between universal (for all moves...) and existential (there is a move...) parts is essential to encode the game; it would be impossible without quantification. Logical formulas like these, in which we are interested, are called (ordinary) quantified Boolean formulas or QBF for short. Dependency QBF is a generalization that corresponds to multiple-player games. Apart from games, QBF and DQBF find their application in areas such as software verification and synthesis, artificial intelligence, and automated design of integrated circuits. This project aims to further the understanding of QBF and DQBF by taking two innovative approaches. First, we want to look at these two concepts jointly. Second, we want to investigate theoretical properties as well as develop practical solvers. Several questions arise on the way: about the relationship between QBF and DQBF; between theoretical concepts and actual solvers; and about smart encodings and their impact on solver performance. The project is situated at the interface of theory and practice, and as such both mathematical work with pen and paper, as well as large-scale computations over clusters with hundreds of processors will be required.

The project's main goal was to advance our understanding of quantified Boolean formulas (QBF) and dependency quantified Boolean formulas (DQBF), which are mathematical representations of complex decision problems. Such formulas are used to model and solve real-world problems in areas like artificial intelligence, optimization, and software and hardware verification and synthesis. This research sought to bridge the gap between theory and practice in the field, as the two have often been developed separately in the past, leading to a lack of proper theoretical foundations for practical advancements. Proof systems are a formal way to study mathematical proofs, and they provide a structured framework for understanding the properties and complexities of different problems. Solvers for hard problems are often too complex to be analyzed directly, but if they can produce formal proofs, they can be understood through them. One significant outcome of the project was a better understanding of the hardness of proving certain mathematical formulas. We were able to map the hardness landscape for resolution, which is one of the most fundamental proof systems in computer science, and which is also used in practice. This work resulted in a dataset containing formulas and proofs, as well as a software tool that can compute the shortest proofs of formulas. These resources can help researchers further investigate the hardness of different problems and potentially develop more efficient algorithms for solving them. Dependency schemes are algorithms that manipulate formulas to make them easier to solve, often by rearranging variables in a problem or discovering hidden causal relationships. They provide valuable insights for developing proof systems and solvers. Within this project we developed new dependency schemes and analyzed them from the point of view of their respective proof systems. Another important finding was the comparison of various QBF-solving algorithms. We studied the power of different algorithms used in state-of-the-art QBF solvers. This research led to the successful implementation of a new feature in the QBF solver Qute. In conclusion, this project has made important strides in bridging the gap between theory and practice in the study of QBF and DQBF. The research has led to a deeper understanding of the hardness of formulas, the development of more efficient solving algorithms, and the introduction of new dependency schemes. These advances have the potential to make a significant impact on the practical applications of QBF and DQBF in solving complex decision problems in various fields.