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

Dit paper introduceert drie nieuwe SAT-coderingen die een middenweg bieden tussen volledig gelift en volledig geground plannen door acties gelift te houden en predicaten gedeeltelijk te grounden, wat leidt tot een lineaire schaalbaarheid met de planlengte en superieure prestaties op moeilijk te grounden domeinen.

De kern

Stel je voor dat je een gigantische, ingewikkelde puzzel moet oplossen. Je hebt een startpunt, een doel en een lijst met regels over wat je mag doen om van A naar B te komen. In de wereld van kunstmatige intelligentie (AI) noemen we dit planning.

De auteurs van dit paper, João Filipe en Gregor Behnke, hebben een nieuwe manier bedacht om deze puzzels sneller op te lossen. Ze noemen hun methode een "gedeeltelijk verankerde codering". Dat klinkt als een moeilijke wiskundetaal, maar laten we het eens proberen uit te leggen met een paar simpele analogieën.

Het Probleem: De "Alles-in-één" Lijst

Stel je voor dat je een reisplanner maakt voor een wereldreis.

• De oude methode (Volledig "Grounded"): Je maakt een lijst met elke mogelijke combinatie van mensen, vliegtuigen en steden. Als er 100 mensen en 100 steden zijn, heb je 10.000 regels nodig om te zeggen wie waar kan zitten. Als je de wereld groter maakt, explodeert deze lijst. Het wordt een onbeheersbare berg papier waar niemand meer doorheen kan kijken.
• De nieuwe methode (Volledig "Lifted"): Je schrijft één algemene regel: "Iedereen kan in elk vliegtuig zitten." Dit is compact en slim. Maar voor de computer is dit soms lastig om direct te rekenen, omdat het te abstract is.

De huidige beste methode (LiSAT) probeert dit slim te combineren, maar heeft een groot nadeel: het groeit te snel.
Stel je voor dat je een route zoekt voor 10 dagen. De computer moet voor elke dag controleren of elke stap logisch is. Bij LiSAT moet de computer voor elke dag alle eerdere dagen opnieuw controleren.

• 1 dag = 1 check.
• 10 dagen = 100 checks.
• 100 dagen = 10.000 checks.
  Dit is een kwadratische groei. Het wordt snel te zwaar voor de computer, net als een raket die te zwaar wordt om de aarde te verlaten.

De Oplossing: De "Gedeeltelijk Verankerde" Sleutel

De auteurs zeggen: "Waarom doen we niet een beetje van beide?"
Ze houden de acties (wat je mag doen) abstract (zoals "Iemand kan vliegen"), maar ze maken de toestand (waar de mensen precies zitten) concreet, maar dan slim.

Hier komt hun creatieve trucje om de hoek kijken: De "Mutex Groep" (De Eén-op-één Regel).

In veel puzzels zijn er regels zoals: "Een pakket kan niet tegelijkertijd in Amsterdam én in Lissabon zijn."
De auteurs gebruiken dit idee. In plaats van voor elk pakket te vragen "Is het in Amsterdam? Is het in Lissabon? Is het in Berlijn?" (wat veel ruimte kost), zeggen ze:
"Er is één 'slot' voor dit pakket. Dat slot kan één van deze steden bevatten."

Ze gebruiken een teller (een variabele) om te zeggen: "Het pakket zit op positie 3 in de lijst van steden."

• Vroeger: Je had een knop voor elke stad (Amsterdam-knop, Lissabon-knop...).
• Nu: Je hebt één knop met een getal erop (3).

Dit is als het verschil tussen het opschrijven van de naam van elke persoon in een zaal (duizenden namen) versus het opschrijven van het aantal mensen in de zaal (één getal).

Waarom is dit beter? (De Lineaire Groei)

Door deze slimme tellers te gebruiken, groeit de hoeveelheid werk voor de computer lineair, niet kwadratisch.

• Vroeger (LiSAT): Als je plan 10 stappen langer wordt, moet de computer 100 keer meer werk doen.
• Nu (Deze paper): Als je plan 10 stappen langer wordt, doet de computer slechts 10 keer meer werk.

Het is alsof je van een trage, kronkelende bergweg (waar je bij elke bocht opnieuw moet kijken) overstapt op een rechte snelweg. Je komt veel sneller aan bij lange routes.

De Drie Variaties

De auteurs hebben drie manieren bedacht om dit te doen, net als drie verschillende soorten gereedschappen:

1. De "Alles-concrete" methode: Ze maken alles concreet. Dit werkt goed voor simpele puzzels, maar faalt bij grote.
2. De "Gedeeltelijk-concrete" methode (One-hot): Ze gebruiken de slimme tellers, maar schrijven de opties nog wel als een lange lijst van knoppen.
3. De "Binaire" methode (De winnaar): Ze gebruiken de slimme tellers en schrijven ze op in binaire code (zoals 001, 010, 100 in plaats van 1, 2, 3). Dit is als het verschil tussen het schrijven van het getal "duizend" (4 letters) versus het schrijven van 1000 (4 cijfers). Het bespaart enorm veel ruimte, vooral bij grote puzzels met veel objecten.

Wat is het resultaat?

In hun tests hebben ze gekeken naar moeilijke puzzels (zoals het verplaatsen van pakketten, robots die data overbrengen, of het oplossen van labyrinten).

• Bij korte puzzels was de oude methode (LiSAT) nog steeds goed.
• Bij lange, moeilijke puzzels wonnen de nieuwe methoden van de auteurs ruimschoots. Ze konden problemen oplossen waar de oude methoden vastliepen.

Samenvattend in één zin:

De auteurs hebben een manier gevonden om AI-planners te laten werken alsof ze een compacte, digitale schuifbalk gebruiken in plaats van een enorme, papieren lijst, waardoor ze veel langere en complexere routes kunnen plannen zonder dat de computer vastloopt.

Het is een beetje alsof je van een handgeschreven adresboek overstapt op een slimme GPS: je hebt dezelfde informatie, maar je kunt er veel sneller en efficiënter mee navigeren.

Technische samenvatting

Probleemstelling

Klassieke planningsproblemen worden doorgaans gedefinieerd met behulp van opgeheven (lifted) eerste-orde representaties, wat compactheid en generaliteit biedt. De meeste planners "grounden" (instantiëren) deze representaties volledig om het redeneren te vereenvoudigen. Dit leidt echter vaak tot een exponentiële toename in grootte, vooral bij complexe domeinen met veel objecten.

Recente benaderingen werken direct op het opgeheven niveau om volledige grounding te vermijden. Een leidende methode hiervoor is LiSAT (Holler en Behnke, 2022), een SAT-encoding die volledig opgeheven werkt. Hoewel LiSAT effectief is voor plannen van optimale lengte, heeft het een fundamenteel nadeel: de grootte van de gegenereerde SAT-formule groeit kwadratisch met de planlengte ($\ell$). Dit komt doordat LiSAT causale links moet coderen tussen acties en precondities zonder de staat expliciet bij te houden. Voor lange plannen wordt dit een schaalbaarheidsprobleem. Anderzijds leidt volledige grounding tot een enorme hoeveelheid feiten en variabelen, wat ook niet schaalbaar is.

Methodologie

De auteurs verkennen een middenweg tussen volledige grounding en volledige lifting door drie nieuwe SAT-encodings te introduceren. De kern van hun aanpak is:

1. Acties volledig opgeheven: Net als LiSAT houden ze acties volledig opgeheven (gebruikmakend van "Unified Arguments" om argumenten van verschillende acties te delen op basis van type).
2. Staat gedeeltelijk grounded: In plaats van causale links te gebruiken, coderen ze de staat expliciet. Ze onderscheiden drie niveaus van grounding voor de predikaten (de staat):
   • Volledig grounded: Alle predikaten worden volledig geïnstantieerd tot feiten (fungeert als baseline).
   • Gedeeltelijk grounded (One-hot): Predikaten worden vertegenwoordigd door Partially Lifted Mutex Groups (PLMGs). Een PLMG is een groep feiten waarvan er in elke bereikbare staat maximaal één waar kan zijn. In plaats van alle mogelijke feiten te coderen, gebruiken ze getelde variabelen om aan te geven welk feit waar is.
   • Gedeeltelijk grounded (Binary): Een verdere optimalisatie waarbij de informatie in de "one-hot" variabelen wordt gecomprimeerd naar een binaire representatie (logaritmisch in het aantal objecten), wat het aantal variabelen drastisch vermindert.

Technische details van de encoding:

• De formule heeft de vorm $F = F_I \land F_G \land \bigwedge_{t=0}^{\ell} \tau(t, t+1)$, waarbij $\tau$ de overgang tussen tijdstappen encodeert.
• Omdat de staat expliciet wordt bijgehouden via PLMGs, is er geen noodzaak voor causale links, wat zorgt voor een lineaire schaling met de planlengte in plaats van kwadratisch.
• Ze gebruiken Predicate Pruning: Predikaten die niet voorkomen in de doelstelling of als preconditie worden verwijderd om de formulegrootte te verkleinen.
• Voor de PLMGs worden specifieke variabelen geïntroduceerd (bijv. (cM = o)t voor de waarde van een getelde variabele, en (pM)t voor welke literaal waar is) en frame-axioma's die garanderen dat de staat alleen verandert door acties.

Belangrijkste Bijdragen

1. Lineaire Schaling: De belangrijkste theoretische bijdrage is het doorbreken van de kwadratische schaling van LiSAT. De nieuwe encodings schalen lineair met de planlengte, wat hen in staat stelt om langere plannen efficiënter te hanteren.
2. Hybride Representatie: Het introduceren van een hybride aanpak waarbij acties opgeheven blijven (voor compactheid) maar de staat gedeeltelijk grounded wordt (voor expliciete staat-tracking zonder kwadratische groei).
3. PLMG-gebaseerde Encoding: Het effectief toepassen van Partially Lifted Mutex Groups om de staat te comprimeren zonder volledige grounding, inclusief een binaire encoding-optimalisatie voor objecten.
4. Empirisch Bewijs: Het aantonen dat deze methode superieur is aan de state-of-the-art (LiSAT) in specifieke, moeilijk te grounden domeinen.

Resultaten

De auteurs hebben hun methoden getest op standaard benchmarks voor opgeheven plannen (zoals Transport, Blocks, Logistics, etc.) en vergeleken met LiSAT, Powerlifted (PWL), CPDDL, en grounded planners (Madagascar, Fast Downward).

• Optimale Planning (Length-Optimal):

  • De nieuwe encodings (vooral de "Binary" variant met Predicate Pruning) presteren beter dan LiSAT in 5 van de 9 geteste domeinen.
  • In domeinen zoals Logistics, Pipesworld en Rover is er een verbetering van meer dan 20% in het aantal opgeloste instanties ten opzichte van LiSAT.
  • Hoewel LiSAT in sommige domeinen (zoals GED en Labyrinth) nog iets beter scoort, zijn de nieuwe methoden daar competitief (verschil < 5%).
  • De totale "score" (som van percentages per domein) is hoger voor de nieuwe methoden dan voor LiSAT.

• Satisficing Planning:

  • In de satisficing modus (niet noodzakelijk optimale lengte) presteert de beste encoding van de auteurs (Binary PP) goed, maar wordt deze overtroffen door zoekgebaseerde methoden zoals PWL.
  • Belangrijk is dat SAT-gebaseerde planners (LiSAT en de nieuwe methode) complementaire vaardigheden bieden: ze lossen problemen op die zoekgebaseerde planners niet aankunnen (bijv. in Blocksworld en Visitall).

• Formulegrootte:

  • De analyse toont aan dat LiSAT kwadratisch groeit in het aantal variabelen en clausules naarmate de planlengte toeneemt, terwijl de nieuwe encoding lineair groeit.
  • Hoewel de nieuwe encoding soms meer clausules genereert dan LiSAT (vanwege de complexiteit van PLMG-semantiek), vereist het aanzienlijk minder variabelen (tot twee ordes van grootte minder), wat cruciaal is voor de schaalbaarheid.

Betekenis en Conclusie

Dit paper biedt een significante doorbraak in SAT-gebaseerd plannen door het "kwadratische probleem" van volledig opgeheven planning op te lossen. De auteurs tonen aan dat het niet nodig is om te kiezen tussen volledige grounding (explosie van feiten) en volledige lifting (explosie van causale links).

De partially grounded encoding biedt een schaalbare oplossing voor lange plannen in complexe domeinen. De resultaten suggereren dat SAT-gebaseerde planners, wanneer ze goed worden geoptimaliseerd, een sterke concurrent zijn voor zoekgebaseerde planners en waardevolle aanvullingen kunnen vormen in een portfolio van planners. De methode is vooral waardevol in domeinen met veel objecten en complexe type-relaties waar volledige grounding onhaalbaar is.

Toekomstig werk richt zich op het integreren van actieparallelisme en het uitbreiden van de encoding naar negatieve precondities en conditionele effecten.