Mein Forschungsschwerpunkt liegt im Bereich der Logik und deren Anwendungen. Dabei beschäftige ich mich insbesondere mit aussagenlogischer Erfüllbarkeit (SAT) und quantifizierten Booleschen Formeln (QBF). Neben mehr als einem Dutzend Veröffentlichungen zu diesen Themen habe ich auch eine umfangreiche Logik-Software namens ProverBox entwickelt.

Darüber hinaus interessiere ich mich für maschinelles Lernen, Data Mining und andere Themen der künstlichen Intelligenz (KI), sowie (Optimierungs-) Algorithmen und Datenstrukturen. Im letztgenannten Bereich habe ich an der Universität Ulm an einem mit einem Forschungspreis ausgezeichneten Projekt zum platzoptimierten Verpacken von Industrie-Garnspulen mitgearbeitet.

Logik und Anwendungen

Ein erfolgreicher Ansatz zum praktischen Lösen schwieriger Entscheidungsprobleme besteht darin, diese in aussagenlogische oder prädikatenlogische Formeln zu übersetzen und dann einen der existierenden Logik-Löser bzw. -Solver einzusetzen. Vor allem aussagenlogische SAT-Solver haben sich in den letzten Jahren zu hocheffizienten Werkzeugen für viele interessante Anwendungen entwickelt. So findet man SAT-Solver beispielsweise im Linux-Paketmanager ZYpp oder dem Eclipse OSGi-Framework.

Eine der wichtigsten Anwendungen für SAT-Solver ist Verifikation. Verifikation ist eine grundlegende Technologie zur Überprüfung, ob Hardware- oder Software-Systeme ihre Spezifikation erfüllen. Moderne Verifikationsverfahren wie Bounded Model Checking (BMC) produzieren aussagenlogische Formeln, die dann gelöst werden müssen.

In der Praxis führt die Übersetzung von Verifikationsproblemen in Aussagenlogik häufig zur Erzeugung sehr großer und damit nur schwer handhabbarer Formeln. Allerdings besitzen diese oft eine sehr spezielle Struktur, beispielsweise könnten sie mehrere Kopien der Zustandsübergangsrelation enthalten.

Quantifizierte Boolesche Formeln

Diese spezielle Struktur lässt sich mit einer mächtigeren Logik ausnutzen. Quantifizierte Boolesche Formeln (QBF) erweitern die Aussagenlogik um die Möglichkeit, aussagenlogische Variablen existenziell oder universell zu quantifizieren. Dies ermöglicht sehr natürliche Problemrepräsentationen, welche oftmals erheblich kompakter als ihre aussagenlogischen Äquivalente sind, aber auch schwieriger zu lösen. Dabei scheinen nicht alle Benutzungsmuster von Quantoren gleich effektiv zu sein, so dass es wichtig ist, einen Kompromiss zwischen Klarheit und Kompaktheit auf der einen und Entscheidungskomplexität auf der anderen Seite zu finden. Meine Forschung untersucht deshalb insbesondere

• Beziehungen zwischen der Formelstruktur und der Ausdrucksmächtigkeit von Quantoren,
• Vorverarbeitungsansätze zur Eliminierung schwacher Quantoren,
• nützliche Teilklassen mit niedrigerer Komplexität,
• sowie geeignete Modellierungsstrategien.

Ich habe dabei die Expansion von Allquantoren genauer betrachtet und gezeigt, dass diese erheblich vereinfacht werden kann, wenn man Variablenabhängigkeiten und die Struktur der Matrix bei Formeln in konjunktiver Normalform (QCNF) berücksichtigt. Im Spezialfall der quantifizierten Hornformeln (QHORN) lässt sich die gleichzeitige Expansion aller Allquantoren sogar in quadratischer Länge durchführen. Ich habe die Allquantorexpansion auch verallgemeinert auf dependency-quantifizierte Boolesche Formeln (DQBF), eine Erweiterung von QBF um Quantoren mit expliziten Variablenabhängigkeiten. Dabei konnte ich zeigen, dass Horn- und 2-CNF-Formeln sogar mit diesen mächtigeren Quantoren polynomial entscheidbar bleiben.

Eine gute Übersicht über die Resultate zu diesem Thema findet sich in meiner Dissertation, die in der Buchreihe DISKI bei IOS Press erschienen ist:

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 Volltext] [Originalveröffentlichung bei IOS Press]

Weitere Veröffentlichungen finden sich in meinem Publikationsverzeichnis.

Logik-Software

In meiner freien Zeit arbeite ich an meiner Logiksoftware ProverBox. Diese bietet eine modulare Plattform zur Integration unterschiedlicher Logiken und Theorembeweiser sowie eine moderne Benutzeroberfläche mit integriertem Editor und Visualisierungsmöglichkeiten.

Die ProverBox enthält auch einen expansionsbasierten QBF-Präprozessor, welcher einige der oben erwähnten Techniken implementiert.

Bei Interesse finden Sie weitere Informationen auf der ProverBox Website.