Entscheidungs- und Optimierungsprobleme für Graphen mit gegebener Baumzerlegung
Final Report Abstract
Der Satz von Courcelle besagt, dass jedes in monadischer Prädikatenlogik zweiter Stufe (MSO) formulierbare Problem auf Graphen mit kleiner Baumweite in Linearzeit lösbar ist. In der Theorie findet dieses Resultat breite Anwendung, etwa im Bereich der parametrisierten Komplexitätstheorie. Das übergeordnete Ziel des vorliegenden Projektes war es, ein praxistaugliches Werkzeug zu entwickeln, welches entsprechend des Satzes von Courcelle für eine große Klasse von graphentheoretischen Problemen einsetzbar ist. Inzwischen ist dieses Werkzeug unter dem Namen "Sequoia" entstanden und steht unter einer liberalen Open-Source-Lizenz öffentlich zur Verfügung. Um das übergeordnete Ziel zu erreichen, musste in drei verschiedenen Bereichen gearbeitet werden. Der erste und zeitlich längste Teil bestand in der Schaffung der theoretischen Grundlagen. Der klassische Beweis beruht auf Automatentheorie und ist zwar konstruktiv, aber entsprechende Versuche anderer, daraus ein Werkzeug zu bauen, zeigten, dass dieser Ansatz zumindest direkt nicht erfolgversprechend ist. Die Konstruktion der Automaten stellte sich als unmöglich heraus. Inzwischen gibt es von Bruno Courcelle ein angepasstes Verfahren, das die Baumautomaten nicht vollständig konstruiert, sondern während ihres Laufs nur soweit aufbaut wie notwendig. Dieser Ansatz hat sich ebenfalls als funktionsfähig herausgestellt. Unser Ansatz war ein spieltheoretischer, welcher ebenfalls sehr darauf achtet, möglichst wenig unnötige Information zu speichern. Es liegt in der Natur dynamischen Programmierens, dass nicht nur das Ergebnis selbst, sondern auch viele weitere Nebenergebnisse berechnet werden. Der spieltheoretische Ansatz führt die Evaluierung einer Formel auf ein Spiel zwischen zwei Spielern zurück. Dabei dürfen sie auch auf dem "noch unbekannten" und "schon vergessenen" Teil des Graphen Züge durchführen, die aber stark abstrahiert werden. Durch sie kann aber der Spielbaum klein gehalten werden. Die sehr teuren Züge werden auf den Knoten eines aktuellen Bags der Baumzerlegung durchgeführt. Dieser grundsätzliche Ansatz kann auf verschiedene Arten umgesetzt werden und im Laufe der Projektlaufzeit wurde er immer wieder modifiziert und dadurch verbessert. Gleichzeitig wurde er auf Erweiterungen von MSO verallgemeinert und auch auf Clique- und Rankwidth-Zerlegungen ausgedehnt. (Letztere wurden nicht implementiert, da wir uns auf Baumzerlegungen konzentrieren wollten.) Im zweiten, praktischen Teil mussten diese Algorithmen korrekt und möglichst effizient implementiert, getestet und evaluiert werden. Dabei wurden Schwachstellen entdeckt, die dann wieder durch theoretische Verbesserungen am Algorithmus repariert wurden; ein Zyklus, der sich immer wieder wiederholte. Um ein wirklich nützliches Werkzeug zu schaffen, mussten in einem kleineren dritten Teil des Projekts schließlich auch Verbesserungen der Implementierung durchgeführt werden, die nicht auf dem Algorithmus beruhten. Hier handelte es sich um Techniken, die zum Beispiel bereits berechnete Ergebnisse effizient in einem Cache halten, besonders angepasste Hashfunktionen, Isomorphietests zwischen Spielbäumen usw. Diese Verbesserungen haben die Laufzeit und den Speicherverbrauch extrem reduzieren können, auch wenn sie asymptotisch eine kleinere Rolle spielen als die rein algorithmischen Verbesserungen. Heute kann man routinemäßig verschiedenste Optimierungs- und Entscheidungsprobleme mit "Sequoia" in kurzer Zeit lösen. Damit ist es zum Beispiel geeignet, schnelle Prototypen zu entwickeln oder Tests für andere Tools zu erstellen. Für Graphen, die gleichzeitig groß sind, aber kleine Baumweite haben, ist "Sequoia" in manchen Szenarien das einzige generische Werkzeug, welches überhaupt zum Ziel führt.
Publications
- A practical approach to courcelle’s theorem. Electr. Notes Theor. Comput. Sci., 251:65–81, 2009
Joachim Kneis and Alexander Langer
(See online at https://doi.org/10.1016/j.entcs.2009.08.028) - Dynamic programming on tree decompositions using generalised fast subset convolution. In Amos Fiat and Peter Sanders, editors, Algorithms - ESA 2009, 17th Annual European Symposium, Copenhagen, Denmark, September 7-9, 2009. Proceedings, volume 5757 of Lecture Notes in Computer Science, pages 566–577. Springer, 2009
Johan M. M. van Rooij, Hans L. Bodlaender, and Peter Rossmanith
(See online at https://doi.org/10.1007/978-3-642-04128-0_51) - Courcelle’s theorem - A game-theoretic approach. Discrete Optimization, 8(4):568–594, 2011
Joachim Kneis, Alexander Langer, and Peter Rossmanith
(See online at https://doi.org/10.1016/j.disopt.2011.06.001) - Linear-time algorithms for graphs of bounded rankwidth: A fresh look using game theory - (extended abstract). In Mitsunori Ogihara and Jun Tarui, editors, Theory and Applications of Models of Computation - 8th Annual Conference, TAMC 2011, Tokyo, Japan, May 23-25, 2011. Proceedings, volume 6648 of Lecture Notes in Computer Science, pages 505–516. Springer, 2011
Alexander Langer, Peter Rossmanith, and Somnath Sikdar
(See online at https://doi.org/10.1007/978-3-642-20877-5_49) - Evaluation of an mso-solver. In David A. Bader and Petra Mutzel, editors, Proceedings of the 14th Meeting on Algorithm Engineering & Experiments, ALENEX 2012, The Westin Miyako, Kyoto, Japan, January 16, 2012, pages 55–63. SIAM / Omnipress, 2012
Alexander Langer, Felix Reidl, Peter Rossmanith, and Somnath Sikdar
- Schnelle Algorithmen für zerlegbare Graphen. In Steffen Hölldobler, editor, Ausgezeichnete Informatikdissertationen 2013, volume D-14 of LNI, pages 101–110. GI, 2013
Alexander Langer
- Practical algorithms for MSO model-checking on tree-decomposable graphs. Computer Science Review, 13-14:39–74, 2014
Alexander Langer, Felix Reidl, Peter Rossmanith, and Somnath Sikdar
(See online at https://doi.org/10.1016/j.cosrev.2014.08.001)
