Research Interests

I am interested in finding and representing models of logical formulae. There might be different ways to represent a model, and which one is adequate depends on the task and on the logic. So, while for example in propositional logic we want to find short models, things become more complicated if quantifiers are involved. So, models in quantified Boolean formulae (QBF) are represented as trees. In predicate logic, models may become infinite, and the challenge is to represent them finitely, which, due to the undecidability of first-order logic, is not always possible. One solution to this issue is to focus on decidable fragments expressive enough for our needs.

My PhD evolved around propositional model counting, also called #SAT, and propositional model enumeration, All-SAT. These are the counting and enumeration variants of the Boolean satisfiability problem (SAT).

When asked was I am precisely working on, I used to explain it as follows: Statements can be represented by means of (propositional) variables. These variables can be either true or false, depending on whether this statement holds or not. For instance, let "the sun is shining" be represented by a variable a and "it is cloudy" by a variable b. If the sun shines, we set a to true, and if it is cloudy, we set b to true. Now we make the following statement: "the sun is shining or it is cloudy." We can express this statement as follows: a OR b. This is a formula, and in SAT we are interested in knowing whether we can assign a and b values such that this formula becomes true.

In natural language, "the sun is shining or it is cloudy" says that either the sun is shining or it is cloudy, but not both. However, the logical OR behaves differently, and our formula a OR b is true if either a is true or b is true or both a and b are true. In other words, our formula is true if either the sun shines or it is cloudy or the sun shines and it is cloudy. So, we have found three possible assignments to our variables such that the formula becomes true. Assignments under which the formula is true are called models. In our example, these are the following: a = true, b = false; a = false, b = true; a = true, b = true. And with this, we already have solved not only the SAT, but also the #SAT and the All-SAT problem.

Still, this example seems too abstract to someone not familiar with mathematical logic. Now it happened that for the 2018 edition of the Lange Nacht der Forschung, Martina Seidl developed the Box Game, which is explained in a very illustrative manner in her slides. The motivation was to bring mathematical logic closer to a broad audience. And it was a big success! Both adults and children set out to solve the Box Game, and many succeeded. To give you an idea of its difficulty: the Box Game is defined over ten variables, each of which can be assigned one out of the two values true and false, and hence the variables can be assigned in 2^10 = 2·2·2·2·2·2·2·2·2·2 = 1'024 different manners. So, solving the Box Game requires some strategy beyond trying out all possible combinations - as is the case for SAT and in particular for #SAT and All-SAT, where we need to find all models. And with this, we also identified one of the main challenges in #SAT and All-SAT: the size of the search space, i.e., the number of possible assignments to be checked, increases exponentially with the number of variables.