Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
Logo Leibniz Universität Hannover
Logo:Institut für Theoretische Informatik
  • Zielgruppen
  • Suche
 

DFG gefördertes Projekt

Dauer: April 2014 - Februar 2018 (Teil 1), Februar 2018 - Februar 2021 (Teil 2)

Beteiligte

Arne Meier (Projektleiter)

Irena Schindler (bis 12-2017)

Nichtklassische Logiken: Parametrisierte Komplexität und Enumeration (DFG Projekt ME 4279/1-2)

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

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.

Parametrisierte Komplexität nicht-klassischer Logiken (DFG Projekt ME 4279/1-1)

Nach heutigem Wissensstand ist nur sehr wenig über die parametrisierte Komplexität im Bereich Programmverifikation und künstlicher Intelligenz bekannt. In diesem Projekt wird sowohl die Parametrisierung als auch der Einfluss der Parametrisierung auf die Komplexität der wichtigen Entscheidungsprobleme, wie z.B. Erfüllbarkeit und Model Checking, untersucht. Im Bereich der nicht-monotonen Logiken werden wir Probleme des natürlichen Schließens betrachten. Darüber hinaus wollen wir Normalformen in Bezug auf die Parametrisierung finden, die die gewöhnlich hohe Komplexität dieser Probleme erklären.

Sensible Parametrisierung:

Wir fokussieren uns auf die Vorteile der Parametrisierung im Bereich der modal Logik, sowie der nicht-monotone Logiken, da es bis jetzt kaum Ansätze dieser Art gibt. Dabei wollen wir die Kenntnisse über die Wechselwirkungen von Parametrisierung mit den Konzepten dieser Logiken verbessern.

Klassifizierung der parametrisierten Komplexität in Bezug auf die Fragmente der temporalen und der nicht-monotonen Logiken:

Es wurden bereits eine enorme Anzahl an Klassifikationen der Komplexität von Fragmenten für jede der genannten Logiken angefertigt. Bei der Klassifizierung der parametrisierten Komplexität dieser Fragmente wollen wir unser Wissen und unsere Intuition über die Wechselwirkungen von modalen, bzw. nichtmonotonen Operatoren mit Booleschen Funktionen vertiefen. Können ähnliche Beobachtungen wie z.B. in der Aussagenlogik gemacht werden?

Einfluss der Nichtmonotonie:

Im letzten Projektabschnitt werden wir die Kenntnisse über die erhaltenen Klassifikationen der vorherigen Abschnitte analysieren, um eine Gesamtübersicht zu erstellen. Insbesondere werden wir uns der Frage widmen, wie das Konzept der Nichtmonotonie sich auf die Effizienz eines Problems auswirkt. Eine der wichtigsten Fragen in diesem Kontext ist, ob es eine inhärente Struktur der Erweiterungen gibt, die in Kombination mit Parametrisierungen, Ineffizienz sogar in der parametrisierten Version des Problems immer erzeugt.

Ausgewählte Publikationen

Johannes K. Fichte, Markus Hecher and Irina Schindler: Default Logic and Bounded Treewidth, accepted at LATA 2018.

Arne Meier, Christian Reinbold: Enumeration Complexity of Poor Man's Propositional Dependence Logic. CoRR abs/1704.03292 (2017)

Martin Lück, Arne Meier, Irena Schindler: Parametrised Complexity of Satisfiability in Temporal Logic. ACM Trans. Comput. Log. 18(1): 1:1-1:32 (2017)

Nadia Creignou, Arne Meier, Julian-Steffen Müller, Johannes Schmidt, Heribert Vollmer: Paradigms for Parameterized Enumeration. Theory Comput. Syst. 60(4): 737-758 (2017)

Arne Meier, Sebastian Ordyniak, Ramanujan Sridharan, Irena SchindlerBackdoors for Linear Temporal LogicIPEC 2016: 23:1-23:17

Johannes Klaus Fichte, Arne Meier, Irina Schindler (2016): Strong Backdoors for Default Logic, Theory and Applications of Satisfiability Testing - SAT 2016 - 19thInternational Conference, Lecture Notes in Computer Science 9710

Martin Lück, Arne Meier (2015): LTL Fragments are Hard for Standard Parameterisations, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015

Andreas Krebs, Arne Meier, Jonni Virtema: A Team Based Variant of CTL. TIME 2015: 140-149

Arne Meier, Irina Schindler, Johannes Schmidt, Michael Thomas, Heribert Vollmer (2015): On the parameterized complexity of non-monotonic logics, Archive for Mathematical Logic, Springer Science + Business Media  

Martin Lück, Arne Meier, Irina Schindler (2015): Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem, Buchtitel: Proc. 9th International Conference on Language and Automata Theory and Applications LATA 2015.