Abschlussarbeit

Zusammenfassung

Klassische Planungssysteme melden lediglich, falls ein Problem unlösbar ist, und liefern keine weiteren Erklärungen. Diese Arbeit überträgt Inkonsistenzmessung aus der Aussagenlogik auf die klassische Planung und stellt strukturelle Diagnostiken der Unlösbarkeit bereit. Eine aussagenlogische Kodierung mit dem Contension- Maß liefert uninformative Ergebnisse und motiviert Maße, die direkt auf Zielen, Operatoren und erreichbaren Zuständen operieren. Drei planungsnative Diagnose- profile mit insgesamt sechs Maßen werden vorgeschlagen. Das Unerreichbarkeitsprofil zählt Zielpropositionen, die in keinem erreichbaren Zustand vorkommen. Das Zielmutex-Profil erkennt operatorinduzierte Ausschlüsse, bei denen Ziele einzeln erreichbar, aber nie gemeinsam erfüllbar sind. Das Zielsequenzierungskonflikt- Profil identifiziert irreversible Ausschlüsse, bei denen das Erreichen eines Ziels ein anderes dauerhaft blockiert. Jedes Profil ist durch einen Planlängenhorizont parametrisiert, wird gegen planungsadaptierte Rationalitätspostulate analysiert und ist PSPACE-vollständig. Die Profile werden mittels Answer Set Programming unter Verwendung von plasp und Clingo-Brave-Reasoning implementiert. Eine experimentelle Auswertung auf Benchmarks der Unsolvability Competition der Inter- national Planning Competition 2016 sowie der Eriksson-Sammlung zeigt, dass die Profile strukturell unterschiedliche Kategorien unlösbarer Instanzen unterscheiden, und offenbart ein Spannungsverhältnis zwischen Genauigkeit und Abdeckung, das der horizontbeschränkten Analyse inhärent ist.