When both Grounding and not Grounding are Bad -- A Partially Grounded Encoding of Planning into SAT (Extended Version)

Die vorgestellte Arbeit stellt drei SAT-Kodierungen vor, die durch eine teilweise Grounding-Strategie einen Mittelweg zwischen vollständigem Grounding und reinem Lifted-Planning schlagen und dabei eine lineare Skalierung bezüglich der Planlänge erreichen, was zu einer verbesserten Leistung bei der Suche nach längenoptimalen Plänen in schwer zu groundenden Domänen führt.

Das Wesentliche

Das große Problem: Der "Alles-und-Jeder"-Planer

Stell dir vor, du möchtest einen Plan erstellen, um eine große Umzugskiste zu packen. Du hast eine Liste von Gegenständen (Bücher, Teller, Klamotten) und Regeln (Teller müssen verpackt werden, Bücher dürfen nicht oben drauf).

In der Welt der künstlichen Intelligenz (KI) gibt es zwei extreme Methoden, solche Pläne zu erstellen:

1. Der "Alles-auswendig-lernende" Planer (Vollständig erdacht/grounded):
   Dieser Planer nimmt jede einzelne Regel und schreibt sie für jeden einzelnen Gegenstand auf.

   • Beispiel: Statt "Packe Teller in die Kiste" schreibt er: "Packe Teller 1 in Kiste A", "Packe Teller 2 in Kiste A", ..., "Packe Teller 1000 in Kiste A".
   • Problem: Wenn du 1000 Teller hast, explodiert die Liste. Sie wird riesig, unübersichtlich und der Computer braucht ewig, um sie zu lesen. Das nennt man "exponentielles Wachstum".

2. Der "Abstrakte Philosoph" (Vollständig gehoben/lifted):
   Dieser Planer denkt nur in allgemeinen Konzepten. Er sagt: "Packe irgendeinen Teller in irgendeine Kiste". Er schreibt keine konkreten Namen auf.

   • Vorteil: Die Liste ist winzig klein.
   • Problem: Um zu prüfen, ob der Plan funktioniert, muss er ständig im Kopf durchrechnen: "Wenn ich Teller 1 nehme, kann ich dann Teller 2 noch nehmen?" Bei langen Plänen (viele Schritte) wird diese Kopfrechenaufgabe so komplex, dass die Liste der Bedingungen quadratisch wächst (also doppelt so schnell wie die Länge des Plans). Das wird bei langen Umzügen auch zu schwer.

Die neue Lösung: Der "Hybrid-Ansatz"

Die Autoren dieses Papers (João Filipe und Gregor Behnke) haben sich gedacht: "Warum müssen wir uns für eine Extreme entscheiden? Warum nicht beides mischen?"

Sie haben eine neue Methode entwickelt, die sie "Partiell erdachte Kodierung" nennen. Stell dir das wie einen cleveren Umzugsleiter vor, der eine hybride Strategie nutzt:

• Die Aktionen bleiben abstrakt (Der Philosoph):
  Der Planer sagt immer noch: "Führe die Aktion 'Packen' aus". Er schreibt nicht sofort "Packe Teller 1", sondern behält die flexible Regel bei. Das spart Platz bei den Anweisungen.
• Der Zustand wird teilweise konkret (Der Praktiker):
  Aber statt sich alles im Kopf vorzustellen, schreibt er sich auf, was gerade passiert. Hier nutzen sie einen cleveren Trick namens "Mutex-Gruppen" (eine Art logisches Sicherheitsnetz).

Die Analogie der "Sitzplätze im Bus"

Stell dir vor, du hast einen Bus (deinen Plan).

• Die alten Methoden versuchten, für jeden Sitzplatz im Bus eine separate Liste zu führen, wer wann wo sitzt. Bei 1000 Sitzplätzen wurde das Papierkram riesig.
• Die neue Methode sagt: "In diesem Bus gibt es eine Gruppe von Sitzen (z. B. die Fensterplätze), von denen nur einer besetzt sein darf."
  • Statt zu schreiben: "Sitz 1 ist frei, Sitz 2 ist frei, Sitz 3 ist besetzt..."
  • Schreibt der Planer nur: "Die Fensterplatz-Gruppe hat den Wert 'Sitz 3'."

Das ist wie ein Schalter, der nur eine Position anzeigt, anstatt 1000 Lichter einzeln zu steuern.

Was bringt das?

1. Lineares Wachstum statt quadratischem:
   Wenn der Plan länger wird (mehr Umzugsstufen), wächst die Komplexität bei der alten Methode (LiSAT) wie ein explodierender Vulkan (quadratisch). Bei der neuen Methode wächst sie wie eine sanfte Rampe (linear). Das bedeutet: Je länger und komplexer der Plan, desto besser schneidet die neue Methode im Vergleich ab.
2. Bessere Ergebnisse bei schweren Aufgaben:
   In Tests mit schwierigen Domänen (wie Logistik oder Robotik) hat ihre Methode (besonders die Variante mit "binärer Kodierung", also einer Art effizienter Binärcode) oft bessere Pläne gefunden als der aktuelle Weltrekordhalter (LiSAT).

Zusammenfassung in einem Satz

Die Forscher haben einen Planer gebaut, der die Kürze abstrakter Regeln mit der Präzision konkreter Listen kombiniert, indem er nur die wirklich wichtigen Details (den Zustand) clever zusammenfasst, statt alles einzeln aufzulisten. Dadurch wird er schneller und effizienter, besonders bei langen und komplizierten Aufgaben.

Das Ergebnis: Ein smarterer KI-Planer, der nicht erstickt, wenn die Aufgabenliste zu lang wird, und der in vielen Fällen schneller zum Ziel kommt als die bisherigen Besten.

Technische Zusammenfassung

1. Problemstellung

Das klassische automatische Planen (Automated Planning) wird oft durch lifted (nicht instanzierte) Repräsentationen definiert, die Kompaktheit und Allgemeingültigkeit bieten. Die meisten Planer grounden (instanziieren) diese Repräsentationen jedoch vollständig, um das logische Schließen zu vereinfachen. Dies führt jedoch in komplexen Domänen mit vielen Objekten zu einer exponentiellen Vergrößerung des Suchraums (Exponential Blowup).

Um dies zu umgehen, wurden lifted Ansätze entwickelt, die direkt auf der nicht instanzierten Ebene operieren. Ein aktueller State-of-the-Art-Ansatz für SAT-basiertes Planen ist LiSAT (Höller & Behnke, 2022). LiSAT vermeidet das vollständige Grounding von Fakten, indem es Aktionen vollständig lifted kodiert und Kausalverknüpfungen (Causal Links) verwendet, um Preconditions zu erfüllen.
Das Hauptproblem: Die Größe der SAT-Formel in LiSAT wächst quadratisch mit der Planlänge ($\ell$), da jede Bedingung mit jedem potenziellen Erzeuger in vorherigen Zeitschritten verknüpft werden muss. Dies limitiert die Skalierbarkeit bei langen Plänen. Andererseits führt das vollständige Grounding von Zuständen (Predikaten) oft zu unhandlich großen Formeln, wenn die Anzahl der Objekte oder die Arität der Predikate hoch ist.

2. Methodik

Die Autoren schlagen einen Mittelweg vor: Partielles Grounding. Das Ziel ist es, Aktionen weiterhin vollständig lifted zu kodieren, während der Zustandsraum (die Prädikate) entweder vollständig oder teilweise (unter Nutzung von Mutex-Gruppen) instanziiert wird.

Kernkonzepte:

• Unified Arguments (UA): Wie in LiSAT werden Argumente von Aktionen basierend auf ihren Typen (nicht ihrer Position) gruppiert, um die Anzahl der Variablen zu minimieren.
• Partially Lifted Mutex Groups (PLMGs): Die Autoren nutzen Lifted Mutex Groups (LMGs), die durch Invarianten definiert sind (z. B. kann ein Paket nicht an zwei Orten gleichzeitig sein). Eine LMG wird zu einer PLMG, wenn die festen Variablen instanziiert sind, die gezählten Variablen (counted variables) jedoch noch lifted bleiben.
• Zustandskodierung: Anstatt alle Fakten explizit als Boolesche Variablen zu kodieren, werden für PLMGs spezielle Variablen eingeführt, die angeben, welches Element der Mutex-Gruppe gerade wahr ist.

Die drei vorgestellten Kodierungen:

1. Fully Grounded Facts: Eine Baseline, bei der alle Prädikate vollständig instanziiert werden (ähnlich klassischen SAT-Planern, aber mit UA und LiSAT-Strukturen).
2. Partially Grounded Facts (One-Hot): Aktionen sind lifted. Für PLMGs werden Variablen eingeführt, die angeben, welches Objekt für eine gezählte Variable gewählt wurde (One-Hot-Encoding: $(c_M = o)_t$).
3. Partially Grounded Facts (Binary): Eine Optimierung der zweiten Methode. Anstatt One-Hot-Variablen zu verwenden, werden die Objekte in Binärcode kodiert ($\lceil \log_2 |O| \rceil$ Variablen pro Objekt). Dies erhöht die Informationsdichte und reduziert die Anzahl der Variablen und Klauseln signifikant bei großen Objektmengen.

Skalierbarkeit:

Ein entscheidender Unterschied zu LiSAT ist die explizite Kodierung des Zustandsübergangs $\tau(t, t+1)$. Da der Zustand explizit verfolgt wird, entfällt die Notwendigkeit, Kausalverknüpfungen über alle Zeitschritte hinweg zu kodieren.

• LiSAT: Formelgröße $\propto \ell^2$ (quadratisch).
• Neue Ansätze: Formelgröße $\propto \ell$ (linear), da die Größe von $\tau(t, t+1)$ konstant bezüglich $\ell$ ist und nur von der Problemgröße $|\Pi|$ abhängt.

Pruning (Beschneidung):

Die Autoren implementieren eine Predicate Pruning-Strategie. Prädikate, die weder im Zielzustand noch als Precondition vorkommen, werden entfernt, um die Anzahl der Fakten zu reduzieren.

3. Wichtige Beiträge

1. Lineare Skalierung: Der Hauptbeitrag ist die Entwicklung von SAT-Kodierungen, die linear mit der Planlänge skalieren, im Gegensatz zum quadratischen Wachstum bei LiSAT.
2. Partielles Grounding: Die Einführung einer hybriden Repräsentation, die die Vorteile von lifted Aktionen (Kompaktheit) mit der Effizienz von teilweise instanziierten Zuständen (Vermeidung von Kausalverknüpfungen) kombiniert.
3. Binäre Kodierung von Objekten: Die Anwendung von Binärcodierung für die Werte innerhalb von PLMGs, um die Variablenanzahl bei großen Domänen drastisch zu senken.
4. Empirische Validierung: Umfassende Experimente, die zeigen, dass diese Ansätze in schwierigen Domänen (schwer zu grounden) den State-of-the-Art übertreffen.

4. Ergebnisse

Die Experimente wurden auf Standard-Benchmarks für lifted Planning durchgeführt (z. B. Transport, Logistik, Rover, Pipesworld) und mit State-of-the-Art-Planern verglichen (LiSAT, Powerlifted, CPDDL, Madagascar, Fast Downward).

• Optimales Planen (Length-Optimal):

  • Die neuen Kodierungen (insbesondere die binäre Variante mit Pruning) übertreffen LiSAT in 5 von 9 Domänen.
  • In Domänen wie Logistics, Pipesworld und Rover konnte die Anzahl der gelösten Instanzen um $\ge 20\%$ gesteigert werden.
  • LiSAT scheitert oft bei längeren Plänen aufgrund des quadratischen Wachstums, während die neuen Ansätze hier skalieren.
  • Die Suchbasierten lifted Methoden (Powerlifted, CPDDL) wurden in diesem Setting von den SAT-basierten Methoden deutlich übertroffen.

• Satisficing Planen:

  • Hier ist LiSAT und Powerlifted (PWL) in der Gesamtabdeckung (Coverage) leicht überlegen, hauptsächlich aufgrund von Domänen mit vielen Instanzen (GED).
  • Dennoch schneiden die neuen Ansätze in spezifischen Domänen (Blocksworld, Childsnack, Visitall, Labyrinth) besser ab als andere lifted und grounded Satisficing-Planer.
  • Dies deutet auf komplementäre Fähigkeiten hin: SAT-Planer lösen Probleme, die für suchbasierte lifted Planer zu schwer sind.

• Formelgröße:

  • Die Anzahl der Klauseln ist bei den neuen Ansätzen oft höher als bei LiSAT (aufgrund der Overhead-Kodierung der PLMG-Semantik), aber die Anzahl der Variablen ist oft deutlich geringer (bis zu zwei Größenordnungen).
  • Das Wachstum der Variablen- und Klauselanzahl ist bei den neuen Ansätzen linear, während LiSAT quadratisch wächst.

5. Bedeutung und Fazit

Das Paper adressiert das fundamentale Dilemma im SAT-basierten Planen: Entweder man groundet alles (exponentielle Explosion) oder man bleibt vollständig lifted (quadratische Skalierung durch Kausalverknüpfungen).

Die vorgestellte Methode des partiellen Groundings bietet eine effiziente Lösung, indem sie die Struktur des Problems (Mutex-Gruppen) nutzt, um den Zustandsraum kompakt darzustellen, ohne die Aktionen zu instanziieren.

• Praktische Relevanz: Die Methode ermöglicht das Lösen von Planungsproblemen in Domänen mit vielen Objekten und langen Plänen, die für LiSAT oder klassische Grounding-Planer unzugänglich sind.
• Zukunft: Die Autoren sehen Potenzial in der Integration von parallelen Aktionen und der Erweiterung auf negative Preconditions und konditionale Effekte.

Zusammenfassend stellt diese Arbeit einen bedeutenden Fortschritt in der Skalierbarkeit von SAT-basiertem Planen dar, indem sie die lineare Skalierung mit der Effizienz von lifted Repräsentationen vereint.