Werkzeuge und Methoden zum Lösen von Problemen mittels Baumweite .

Abstract

In den letzten Jahrzehnten konnte ein beachtlicher Fortschritt im Bereich der Aussagenlogik verzeichnet werden, der sich durch überwältigend schnelle Computerprogramme (Solver) zur Lösung aussagenlogischer Formeln äußert. Einer der Gründe dieser Schnelligkeit befasst sich mit strukturellen Eigenschaften von Probleminstanzen, zum Beispiel der sogenannten Baumweite, wel- che versucht zu messen, wie groß der Abstand von Probleminstanzen zu einfachen Strukturen (Bäumen) ist. Diese Arbeit befasst sich mit Problemen der Künstlichen Intelligenz (KI) sowie Baumweite- basierenden Methoden und Werkzeugen zum Lösen dieser. Wir präsentieren einen neuen Typ von Problemreduktion, den wir als ”zerlegungsangeleitet“ bezeichnen. Dieser ist die Basis, um eine lange offen gebliebene Frage betreffend quantifizierter, aussagenlogischer Formeln (QBF) bei beschränkter Baumweite zu zeigen. Die Lösung der Frage ermöglicht ein neues Meta-Werkzeug zum Beweisen präziser unterer Laufzeitschranken einer Vielzahl von Problemen der KI. Trotz dieser Schranken implementieren wir einen Solver für Erweiterungen von Sat, der Baumweite effizient ausnutzt.