Quantified Boolean Formulas
Verification is crucial for building reliable hardware or software systems. State-of-the-art verification techniques like bounded model checking produce propositional formulas and require determining their satisfiability.
In real-life applications, those formulas tend to be very large, which makes them quite difficult to handle. However, they often have a very special structure. For example, they might contain multiple copies of the transition relation.
It is possible to exploit that special structure in a more sophisticated logic. Quantified Boolean Formulas (QBF) enhance propositional logic by allowing quantifiers over variables. This often allows a natural translation of the original problem into logic. Additionally, quantifiers can be used to introduce abbreviations for repeating parts of a formula. Accordingly, QBF offers a concise way to represent formulas which arise in areas such as verification, planning or scheduling.
QBF: Research Topics
The enhanced capabilities of QBF come at a price: determining the satisfiability of formulas in QBF is PSPACE-complete, which is assumed to be significantly harder than the NP-completeness of the propositional SAT problem. My research focus is therefore on tractable subclasses of QBF. In particular, I consider Quantified Horn Formulas (QHORN), which often occur as subproblems when solving arbitrary QBF formulas. That makes it rewarding to learn more about their structure, to look for efficient algorithms for solving or transforming them and to investigate the relationship between QHORN and QBF.
Another interesting topic which I am exploring is the interplay between the existential and universal variables in QBF formulas. The concept of Satisfiability Models is used to characterize the satisfying truth assignments to the existential variables. Knowing about the structure of those models for certain classes of formulas can make it possible to transform these formulas into simplified equivalent formulas by eliminating, expanding or substituting quantified variables.
In addition, I investigate variants/extensions of QBF, such as non-prenex QBF or Dependency Quantified Boolean Formulas (DQBF).
Logic Software
Whenever I have some spare time, I work on my logic software ProverBox. It is an extensible platform which integrates different logics and different theorem proving algorithms. In addition, the ProverBox provides a modern user interface with an integrated editor and visualization capabilities.
If you are interested, please have a look at the ProverBox website.