Abgeschlossene Forschungsprojekte

Abstract: Im üblichen Vorlesungsbetrieb kommt eine große Anzahl von Menschen zusammen und verbringt diese Zeit großteils im Rezeptionsmodus. Vorne steht die bzw. der Lehrende und trägt vor. In mathematischen Veranstaltungen, in denen Beweise präsentiert werden, ist es nahezu unmöglich, das richtige Tempo zu finden, damit alle Zuhörerinnen und Zuhörer folgen können. Nach der Veranstaltung gehen alle nach Hause und es entstehen Fragen beim Nacharbeiten des Stoffes. Das Konzept der Flipped Lecture bzw. des Inverted Classroom setzt genau hier an, um die Präsenzzeit sinnvoller und effektiver zu nutzen. Mit Hilfe von Videos und anderen Lernmaterialien wird der Stoff in kleinen Lerngruppen oder alleine vor der eigentlichen Veranstaltung bearbeitet und verstanden, um in der Präsenzzeit dann direkt die entstandenen Fragen zu diskutieren und Verständnislücken zu schließen. Dieses Konzept ist didaktisch anerkannt. [1]
In diesem Projekt wurde die Lehrveranstaltung „Komplexität von Algorithmen“, welche Bestandteil im Pflichtcurriculum der Studiengänge Informatik und Technische Informatik der Leibniz Universität Hannover ist, nach dieser Methode durchgeführt. Es nahmen etwa 300 Studierende an der Lehrveranstaltung teil. Traditionell bestand das Modul aus Vorlesungs- und Übungseinheiten. Im Sommersemester 2019 wurde eine Pilotphase mit alten Vorlesungsaufzeichnungen in der Veranstaltung „Komplexität von Algorithmen“ durchgeführt. Durch die begleitende Evaluation über Teaching Analysis Poll (TAP), zwei Lehrbesuche durch Didaktikerinnen bzw. Didaktiker und die Lehrevaluation zeigte sich eine hochgradig positive Akzeptanz durch die Studierenden aufgrund der Verbesserung der Lernsituation. Im Rahmen dieses Projektes wurden Videos und Lernmaterialien didaktisch sinnvoll aufbereitet sowie Teile der Veranstaltung optimiert.

[1] J. Werner, S. Bayer, C. Ebel und C. Spannagel, Hrsg., Flipped Classroom - Zeit für deinen Unterricht, Bertelsmann Stiftung, 2018.

Abstract: Die Theorie der parametrisierten Komplexität (Downey, Fellows 1999) betrachtet sogenannte Parametrisierungen, um die inhärente Schwierigkeit von Problemen besser zu verstehen. Ein einfaches Beispiel für eine solche Parametrisierung ist für das Erfüllbarkeitsproblems aussagenlogischer Formeln (SAT) die Anzahl der Variablen einer gegebenen Formel. Unter dieser Parametrisierung kann man SAT in einer Laufzeit von 2•|Vars(F)|•|F| lösen, wenn F die gegebene Formel ist. Solche Laufzeiten bezeichnet man als "fixed-parameter tractable" (oder kurz, in FPT). Das bedeutet, wenn der Parameter als konstant gesehen wird, ist die Laufzeit polynomiell und der Grad des Polynoms hängt nicht vom Wert des Parameters ab. Im Gegensatz hierzu stehen Laufzeiten der Form n•f(k) deren zugehörige Probleme in der Klasse XP zusammengefasst werden (für Eingabelänge n). Zwischen FPT und XP existiert eine Hierarchie sogenannter "Weft"-Klassen W[i]. Es ist nicht bekannt, ob jegliche der Inklusionen von W[i] zu W[i+1] strikt ist oder ob FPT strikt in W[1] enthalten ist.

Zählprobleme spielen eine Schlüsselrolle bei vielen Durchbrüchen in der strukturellen Komplexitätstheorie. Vor einer Dekade haben Flum und Grohe (2002) eine Theorie von parametrisierten Zählproblemen entwickelt. Flum und Grohe zeigten, dass das Zählen von Zyklen der Länge k in einem gerichteten Graph vollständig für die Klasse #W[1] ist (welches die Zählversion der Klasse W[1] ist; üblicherweise werden hier die Anzahl von akzeptierenden Pfaden gezählt). Weiterhin wurde das Zählen von Lösungen von Model-Checking-Problemen über erststufiger Logik verwendet, um die sogenannte #A-Hierarchie zu charakterisieren. Trotz intensivem Forschungsaufwand blieb bisher ein Erfolg aus, klassische Resultate, wie zum Beispiel den Satz von Toda in die parametrisierte Welt zu übersetzen.

In der deskriptiven Komplexitätstheorie werden Komplexitätsklassen durch Mengen von Formeln charakterisiert. In einem bahnbrechenden Resultat zeigte Fagin (1973), dass die Klasse NP mit der Menge aller existentiellen zweitstufigen Formeln zusammenfällt. Von Immerman (1982) ist eine Charakterisierung der Klasse P bekannt sowie, dass reguläre Sprachen durch monadische zweitstufige Formeln (MSO) charakterisiert werden können. Saluja und Subrahmaniam (1998) erreichten eine logische Charakterisierung von #P durch das Zählen von Modellen einer FO Formel. Darüber hinaus klassifizierte Kontinen (2008) die Zählhierarchie durch Logiken mit verallgemeinerten Quantoren. Flum und Grohe zeigten 2003, dass logische Charakterisierungen von klassischen Komplexitätsklassen, wie P, NP und PSPACE auch auf den parametrisierten Ansatz übertragen werden können. Des Weiteren gaben sie 2007 eine logische Charakterisierung der W*-Hierarchie an.

In diesem Projekt wollen wir parametrisierte Entscheidungs- und Zählklassen durch Mengen logischer Formeln charakterisieren. Wir unterteilen das Projekt in zwei Abschnitte.

Charakterisierung von parametrisierten Komplexitätsklassen
Wie bereits erwähnt besitzt die W*-Hierarchie eine Fagin-artige Charakterisierung durch logische Formeln. Jedoch gibt es bisher keinen solchen Ansatz für die W-Hierarchie, für FPT oder andere bzgl. Parallelität und Platz beschränkte Klassen. Wir planen logische Charakterisierungen von FPT und parametrisierten Varianten von Komplexitätsklassen, wie para-AC[0], para-WNC[1], para-WL und para-WNL welche von Elberfeld, Stockhusen und Tantau (2015) definiert wurden, zu finden.
Charakterisierung von parametrisierten Zählklassen
Bisher sind keine logischen Charakterisierungen von den von Flum und Grohe eingeführten parametrisierten Zählklassen bekannt. Wir beabsichtigen Klassen innerhalb der #W[P] Hierarchie zu beschreiben. Genauer, wir werden an folgenden Fragestellungen arbeiten:
Finde Charakterisierungen von #W[1] und #W[P] bzgl. Zählen über FO oder andere zugehörige Logiken.
Finde logische Charakterisierungen der parametrisierten Analogen der Polynomialzeithierarchie von Montoya (2008).
Versuche die logische Charakterisierung der Zählhierarchie von Kontinen (2009) auf die parametrisierte Fragestellung zu übertragen.
Innerhalb beider Abschnitte werden wir Parametrisierungen natürlicher Zählprobleme, wie das Zählen von Pfaden in gerichteten Graphen oder Pfade in Kellerautomaten, genauer untersuchen. Außerdem stellt sich die Frage wie Werkzeuge der endlichen Modelltheorie (Lokalität, Ehrenfeucht-Fraïssé Spiele, Zero-One Laws, ...) genutzt werden können, um Antworten zu den obigen Fragen zu finden.

Abstract: Die Theorie der parametrisierten Komplexität beschäftigt sich primär mit Problemen, die nicht in Polynomialzeit gelöst werden können. Wie der Name schon sagt, untersucht man für die Praxis relevante Parametrisierung des Problems. Das Ziel ist es einen Parameter zu finden, sodass das Problem in einer Laufzeit gelöst werden kann, welche als ein Produkt von einem Polynom der Eingabelänge und einer beliebigen Funktion im Parameter dargestellt werden kann. In diesem Fall spricht man von einem Problem, welches, engl., fixed parameter tractable ist.

Backdoors
Ein sehr interessanter Parameter sind Hintertüren, sogenannte Backdoors. Diese Hintertüren sollen bildlich eine Abkürzung zu einem effizient lösbaren Unterfall des Problems liefern. In der temporalen Logik, die ein fundamentales Werkzeug im Bereich der Programmverifikation ist, wurden im vorherigen Projekt solche Hintertüren untersucht. Im Folgeprojekt soll nun weiter an diesem Konzept geforscht werden. Ziel ist es eine passende Definition zu finden, welche praxistauglicher ist und enger mit den temporalen Konzepten verwoben wird. Auch in der Default Logik, eine nichtmonotone Logik, welche in den Bereichen der künstlichen Intelligenz verwendet wird, wurde eine stimmige Definition im vorherigen Projekt gefunden. Nun soll neben einer präzisen Klassifikation der so parametrisierten Probleme auch die Anwendbarkeit von sogenannten QBF-Solvern untersucht werden. QBF-Solver sind Programme, die eine komplexere Art von aussagenlogischen Formeln versucht zu lösen. Diese Art von Formeln können (vermutlich, das heißt, unter sinnvollen komplexitätstheoretischen Annahmen) deutlich stärkere Probleme formalisieren. Die Forschung um QBF-Solver ist noch recht jung verglichen mit den hoch optimierten SAT-Solvern (die das prominente Problem der Erfüllbarkeit aussagenlogischer Formeln lösen).

(Parametrisierte) Enumeration und Dependence Logik
Abhängigkeiten, seien es auf funktionaler Ebene, spielen eine Rolle in Bereich von Datenbanken. Jedoch auch andere Gebiete, wie beispielsweise die Spieltheorie oder auch physikalische Eigenschaften lassen sich mit diesem Werkzeug modellieren. Bisher gibt es noch keine Untersuchungen der parametrisierten Komplexität von Problemen in dieser Logik. Wir möchten eine aussagenlogische Variante dieser Logik nun genauer analysieren. In diesem Abschnitt wollen wir uns auch mit der algorithmischen Fragestellung der (parametrisierten) Enumeration beschäftigen. Häufig ist es interessant die günstigste Lösung oder auch die k-te Lösung bezüglich einer bestimmten Ordnung zu kennen. Enumeration für nichtklassische Logiken, wie wir sie in diesem Projekt untersuchen, ist bisher nur sehr wenig in der Forschung betrachtet worden. Wir wollen diese Lücke schließen und bestimmte, nichtmonotone Formalismen dahin gehend klassifizieren. Diese Analyse dient außerdem dazu Enumeration als Aufgabe an sich besser zu verstehen.