Adaptiv-inkrementelle Unifikation by Armin Wolf GMD FIRST, Berlin, Germany Abstract Der Einsatz constraintlogischer Programmierung zur Lösung praktischer dynamischer Constraint- probleme erfordert Lösungsverfahren, die sich im besonderen durch zwei Eigenschaften auszeich- nen sollten: Effizienz: Der Aufwand für die Lösungsanpassung soll proportional zur Größe der Änderung und im allgemeinen geringer sein als der Aufwand für eine vollständige Neuberechnung. Stabilität: Die angepaßte Lösung soll möglichst ähnlich zur vorherigen Lösung sein. Für den Einsatz constraintbasierter Problemlösungen in interaktiven oder reaktiven Systemen in dynamischen Umgebungen, wie zum Beispiel bei der Planung, Konfiguration und im Graphik/De- sign-Bereich, sind beide Punkte gleichermaßen wichtig: Reaktions- und Antwortzeiten nach Änderungen sind zu minimieren, damit das System on-line einsetzbar ist. Änderungen von Plänen, Entwürfen, Layouts und Graphiken sind möglichst zu vermeiden, um Umorganisationen, Umbestellungen, Umorientierungen zu reduzieren (siehe beispielsweise [5, 17]). Um beiden Anforderungen gerecht zu werden, kommen im allgemeinen inkrementelle Verfahren [15] zur Bearbeitung dynamischer Constraintprobleme zum Einsatz. Diese versuchen, eine zuvor berechnete Lösung so anzupassen, daß sie der veränderten Problemstellung genügt. Idealerweise soll das inkrementelle Verfahren zur Lösung dynamischer Constraintprobleme auch adaptiv sein: - Die angepaßten Lösungen sollen sich durch größtmögliche Stabilität auszeichnen, das heißt, sie sollen sich so wenig wie möglich von den ursprünglichen Lösungen unterscheiden. - Die erzielbaren Effizienzsteigerungen des inkrementellen Verfahrens gegenüber einer vollstän- digen Neuberechnung sollen bei der Lösungsanpassung um so größer sein, je geringer die Veränderungen an der Problemstellung sind. Erfolgt die Lösung der Constraintprobleme mit Hilfe von Constraint Handling Rules (CHRs) [1, 2, 10] kann eine Lösungsanpassung bei dynamischen Änderungen nur dann adaptiv erfolgen, wenn dies für die zugrundegelegten built-in Constraints möglich ist. Da syntaktische Gleichungen immer zu den built-in Constraints gehören (vergleiche [1]), wurde untersucht, ob eine möglichst stabile und effiziente Anpassung der Lösungen von syntaktischen Gleichungen erfolgen kann. In dieser Arbeit wird ein adaptiv-inkrementelles Unifikationsverfahren vorgestellt, das für ein Sys- tem syntaktischer Gleichungen entscheidet, ob es in der Menge der rationalen Bäume (rational trees [7]) lösbar ist. Bei Lösbarkeit wird das System in eine Lösungsform (rational solved form [12]) überführt. Wird das System um zusätzliche Gleichungen erweitert, wird bei Lösbarkeit auch die Lösungsform erweitert. Werden Gleichungen aus dem System entfernt, werden nur die davon betroffenen Gleichungen aus der Lösungsform entfernt und gegebenenfalls durch andere ersetzt.