Nichtklassische Logiken: Parametrisierte Komplexität und Enumeration

• Antragsteller: Privatdozent Dr. Arne Meier
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 247444366

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. 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). Die zweite Hälfte des Projekts beschäftigt sich mit der 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.

• DFG-Verfahren: Sachbeihilfen