Inhaltszusammenfassung:
Das Erfüllbarkeitsproblem der Aussagenlogik (SAT) ist nicht nur in der theoretischen Informatik ein grundlegendes Problem, da alle NP-vollständigen
Probleme auf SAT zurückgeführt werden können. Durch die Entwicklung von sehr effizienten SAT Lösern sind in den vergangenen 15 Jahren auch eine Vielzahl
von praktischen Anwendungsmöglichkeiten entwickelt worden. Zu den bekanntesten gehört die Verifikation von Hardware- und Software-Bausteinen.
Bei der Berechnung von unerfüllbaren SAT-Problemen sind Entwickler und Anwender oftmals an einer Erklärung für die Unerfüllbarkeit interessiert.
Eine Möglichkeit diese zu ermitteln ist die Berechnung von minimal unerfüllbaren Teilformeln. Es sind drei grundlegend verschiedene Strategien zur Berechnung
dieser Teilformeln bekannt: mittels Einfügen von Klauseln in ein erfüllbares Teilproblem, durch Entfernen von Kauseln aus einem unerfüllbaren Teilproblem und eine
Kombination der beiden erstgenannten Methoden.
In der vorliegenden Arbeit entwickeln wir zuerst eine interaktive Variante der Strategie, die auf Entfernen von Klauseln basiert. Sie ermöglicht es den Anwendern
interessante Bereiche des Suchraumes manuell zu erschließen und aussagekräftige Erklärung für die Unerfüllbarkeit zu ermitteln. Der theoretische Hintergrund, der
für die interaktive Berechnung von minimal unerfüllbaren Teilformeln entwickelt wurde, um dem Benutzer des Prototyps unnötige Schritte in der Berechnung der
Teilformeln zu ersparen werden im Anschluss für die automatische Aufzählung von mehreren minimal unerfüllbaren Teilformeln verwendet, um dort die aktuell
schnellsten Algorithmen weiter zu verbessern. Die Idee dabei ist mehrere Klauseln zu einem Block zusammenzufassen.
Wir zeigen, wie diese Blöcke die Berechnungen von minimal unerfüllbaren Teilformeln positiv beeinflussen können. Durch die Implementierung eines Prototypen, der
auf den aktuellen Methoden basiert, konnten wir die Effektivität unserer entwickelten Ideen belegen.
Nachdem wir im ersten Teil der Arbeit grundlegende Algorithmen, die bei unerfüllbaren SAT-Problemen angewendet werden, verbessert haben, wenden wir uns im zweiten
Teil der Arbeit neuen Anwendungsmöglichkeiten für SAT zu. Zuerst steht dabei ein Problem aus der Bioinformatik im Mittelpunkt. Wir lösen das sogenannte
Kompatibilitätproblem für evolutionäre Bäume mittels einer Kodierung als Erfüllbarkeitsproblem und zeigen anschließend, wie wir mithilfe dieser neuen Kodierung
ein nah verwandtes Optimierungsproblem lösen können. Den von uns neu entwickelten Ansatz vergleichen wir im Anschluss mit den bisher effektivsten Ansätzen das
Optmierungsproblem zu lösen. Wir konnten zeigen, dass wir für den überwiegenden Teil der getesteten Instanzen neue Bestwerte in der Berechnungszeit erreichen.
Die zweite neue Anwendung von SAT ist ein Problem aus der Graphentheorie, bzw. dem Graphenzeichen. Durch eine schlichte, intuitive, aber dennoch effektive Formulierung
war es uns möglich neue Resultate für das Book Embedding Problem zu ermitteln. Zum einen konnten wir eine nicht triviale untere Schranke von vier für die
benötigte Seitenzahl von 1-planaren Graphen ermitteln. Zum anderen konnten wir zeigen, dass es nicht für jeden planaren Graphen möglich ist, eine Einbettung in
drei Seiten mittels einer sogenannten Schnyder-Aufteilung in drei verschiedene Bäume zu berechnen.
Print-on-Demand