My research focus is on logic and applications, in particular propositional satisfiability (SAT) and quantified Boolean formulas (QBF). Besides more than a dozen of publications on the subject, I have also implemented an extensive logic software platform, called ProverBox.

In addition, I am interested in machine learning, data mining and other topics from artificial intelligence (AI), as well as (optimization) algorithms and data structures in general. In the latter area, I have contributed to an award-winning research project on automated bin packing at the University of Ulm.

Logic and Applications

A popular approach for solving difficult decision problems is to encode them as propositional or predicate logic formulas and to apply one of the powerful logic solvers available today. In particular, propositional SAT solvers have become highly efficient tools for many interesting applications. For example, SAT solvers can be found in the Linux package manager ZYpp or the Eclipse provisioning system.

One of the most prominent applications of SAT solving is verification. Verification is a crucial technique for checking whether hardware or software systems meet their specification. State-of-the-art verification techniques like bounded model checking (BMC) produce propositional formulas and require determining their satisfiability.

In real-life applications, the encoding of verification problems into propositional logic tends to create very large formulas, making them quite difficult to handle. However, they often have a very special structure. For example, they might contain multiple copies of the transition relation.

Quantified Boolean Formulas

It is possible to exploit that special structure in a more sophisticated logic. Quantified Boolean Formulas (QBF) enhance propositional logic by allowing universal and existential quantifiers over propositional variables. This permits very natural encodings which are often significantly more compact than their propositional counterparts, but also more difficult to solve. Not all usage patterns of quantifiers seem equally effective, which makes it important to balance clarity and conciseness versus decision complexity. My research is therefore especially focused on 

  • relationships between formula structure and quantifier expressiveness,
  • preprocessing that eliminates weak quantifiers,
  • useful subclasses with lower complexity,
  • and suitable encoding patterns.

In particular, I have considered the expansion of universal quantifiers and have shown that it can be significantly simplified by considering variable dependencies and the structure of the matrix for formulas in conjunctive normal form (QCNF). Most importantly, universal expansion can be made tractable for Quantified Horn Formulas (QHORN). I have also extended universal expansion to Dependency Quantified Boolean Formulas (DQBF), a further generalization of QBF by allowing quantifiers with explicit variable dependencies. I could prove that Horn and 2-CNF formulas remain tractable even with these more powerful quantifiers.

A good overview of results on this topic can be found in my dissertation, which has appeared in the DISKI book series by IOS Press:

U. Bubeck.
Model-Based Transformations for Quantified Boolean Formulas.
In: Dissertations in Artificial Intelligence (DISKI), Vol. 329, Wolfgang Bibel (Ed.), IOS Press / Akademische Verlagsgesellschaft AKA, Amsterdam NL / Heidelberg DE, ISBN 978-1-60750-545-7, 2010.
[PDF Full Text] [Original Publication at IOS Press]

More publications can be found on my publication list.

Logic Software

ProverBox LogoWhenever 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.

The ProverBox also includes an expansion-based QBF preprocessor which implements some of the techniques mentioned above.

If you are interested, please have a look at the ProverBox website.