ISBN 9783843915557

978-3-8439-1555-7, Reihe Informatik

Robert Zeranski
Satisfiability Characterizations of Upward Planarity Problems

210 Seiten, Dissertation Friedrich-Schiller-Universität Jena (2014), Softcover, A5

Zusammenfassung / Abstract

Gerichtete Graphen können zur Modellierung vieler praktischer Probleme verwendet werden. Deshalb dienen solche Graphen oft zur Lösung oder visuellen Darstellung dieser Probleme. Die Visualisierung gerichteter Graphen kann unter bestimmten Einschränkungen geschehen, dabei interessieren wir uns für Aufwärtszeichnungen. Das sind spezielle Zeichnungen, in denen alle Kanten durch monoton steigende Kurven in der Ebene dargestellt werden. Solche Aufwärtszeichnungen können kreuzungsfrei (aufwärtsplanar) sein oder Kreuzungen enthalten. Deswegen ist es neben der Aufwärtseigenschaft wünschenswert den Graphen ebenfalls mit möglichst wenigen Kreuzungen zu zeichnen. Da wir demnach die Anzahl der Kreuzungen in einer Aufwärtszeichnung minimieren wollen, nennen wir dieses Problem entsprechend Aufwärtskreuzungsminimierung. Sind wir hingegen lediglich an einer kreuzungsfreien Aufwärtszeichnung interessiert, so nennen wir das zugrunde liegende Entscheidungsproblem Aufwärtsplanarität. Eine weiteres Problem ist die Minimierung der Anzahl an Kanten die im Graphen entfernt werden müssen um eine aufwärtsplanare Zeichnung zu ermöglichen. D.h. wir suchen nach einem aufwärtsplanaren Teilgraphen mit maximaler Kantenanzahl.

In dieser Arbeit beschäftigen wir uns mit allen drei Problemen, welche wir als Aufwärtsplanaritätsprobleme zusammenfassen können. Dazu charakterisieren wir das Problem der Aufwärtsplanarität durch aussagenlogische Formeln. D.h. wir konstruieren zu einem gegebenen Graphen G eine Formel F, so dass G genau dann eine aufwärtsplanare Zeichnung erlaubt, wenn die Formel F erfüllbar ist. Diese Charaterisierung basiert auf dem neu eingeführten Konzept der geordneten Einbettungen und erlaubt eine Erweiterung für die Aufwärtskreuzungsminimierung und das Finden eines aufwärtsplanarem Teilgraphen mit maximaler Anzahl an Kanten. Eine solche Charaterisierung erlaubt es uns außerdem, die Aufwärtsplanaritätsprobleme mit Methoden der Erfüllbarkeit zu lösen (durch sogenannte SAT- bzw. PBS-Solver). Durch eine umfangreiche experimentelle Studie werden wir die praktische Tauglichkeit und die Grenzen dieses Ansatzes aufzeigen, was auch den Vergleich zu anderen bereits bekannten Ansätzen für diese Probleme beinhaltet. Insbesondere sind wir nun in der Lage die Qualität aktueller Heuristiken für die Aufwärtskreuzungsminimierung zu untersuchen, da wir -nach bestem Wissen - den ersten exakten deterministischen Ansatz für dieses Problem präsentieren.