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

Questo lavoro propone una codifica SAT parzialmente fondata che mantiene le azioni sollevate e riduce le predizioni parzialmente, ottenendo una scalabilità lineare rispetto alla lunghezza del piano e superando lo stato dell'arte nella pianificazione ottima in lunghezza per domini difficili da fondare.

L'essenziale

Immagina di dover organizzare un enorme viaggio per un gruppo di amici, ma invece di scrivere un piano dettagliato per ogni singola persona, devi creare un piano "universale" che funzioni per chiunque. Questo è il cuore del pianificazione automatica: trovare una sequenza di azioni per passare da una situazione iniziale a un obiettivo desiderato.

Fino a poco tempo fa, i computer risolvevano questi problemi "appiattendo" tutto: prendevano ogni possibile combinazione di persone e luoghi e scrivevano un piano specifico per ognuna. È come se, per organizzare una cena, scrivessi un menu separato per ogni possibile combinazione di ospiti, anche se non sai chi verrà. Il risultato? Un numero di pagine così enorme da far esplodere la memoria del computer (un "esplosione esponenziale").

Recentemente, alcuni ricercatori hanno provato a non scrivere nulla di specifico, usando solo regole generali (come "se c'è un ospite, portagli un piatto"). Questo è più efficiente, ma ha un difetto: per pianificare viaggi lunghi, il computer impiega troppo tempo a collegare le regole tra loro, come se dovesse controllare ogni singolo filo di una rete gigante.

La soluzione di questo paper: Il "Metodo Ibrido"

Gli autori, Jo˜ao Filipe e Gregor Behnke, hanno trovato una via di mezzo intelligente. Immagina di organizzare il viaggio così:

1. Le Azioni Restano "Magiche" (Lifted): Le azioni (come "guidare", "prendere un pacco") restano generali. Non diciamo "Guida l'auto 1 verso Roma", ma diciamo "Guida un'auto verso una città". Questo mantiene il piano compatto.
2. Lo Stato diventa "Parzialmente Concreto" (Partially Grounded): Qui sta la magia. Invece di elencare ogni singolo fatto possibile (es. "Il pacco è a Roma", "Il pacco è a Milano"), usano dei gruppi di sicurezza (chiamati Mutex Groups).
   • L'analogia: Immagina che ogni pacco possa essere in una sola città alla volta. Invece di scrivere 100 frasi diverse per dire dove non è il pacco, diciamo semplicemente: "Il pacco è in una delle città della lista, e solo una di queste è vera".
   • Usano un sistema di "codici" (come un codice a barre o un numero binario) per indicare quale città è quella giusta, invece di scrivere una frase per ogni città.

Perché è meglio?

• Il vecchio metodo (LiSAT): Era come costruire un muro di mattoni per ogni giorno del viaggio. Se il viaggio durava 10 giorni, il muro era piccolo. Se durava 100 giorni, il muro diventava quadruplo e gigantesco (crescita quadratica).
• Il nuovo metodo: È come costruire un muro che cresce solo in altezza, ma la sua larghezza rimane fissa. Ogni giorno aggiungi un solo mattone, indipendentemente da quanto lungo è il viaggio (crescita lineare).

Cosa hanno scoperto?

Hanno testato il loro metodo su problemi difficili, come il trasporto di pacchi o la logistica.

• Risultato: Il loro metodo è stato più veloce e ha risolto più problemi dei migliori metodi esistenti, specialmente quando i viaggi (i piani) dovevano essere lunghi.
• L'effetto "Potatura": Hanno anche scoperto che, prima di iniziare, potevano tagliare via le regole inutili (come le regole per oggetti che non servono mai per raggiungere l'obiettivo), rendendo il compito ancora più leggero.

In sintesi

Immagina di dover scrivere un manuale di istruzioni per un robot.

• Metodo vecchio: Scrivi un capitolo intero per ogni possibile oggetto che il robot potrebbe toccare. Il libro diventa enorme.
• Metodo nuovo: Scrivi un capitolo generale su "come toccare gli oggetti", ma usi un sistema di etichette intelligenti per dire dove sono gli oggetti, senza dover scrivere tutto a mano.

Questo approccio "ibrido" permette ai computer di pianificare viaggi molto più lunghi e complessi senza andare in tilt, rendendo l'intelligenza artificiale più efficiente nel risolvere problemi del mondo reale.

Sommario tecnico

1. Il Problema

Il pianificazione automatica classica (Classical Planning) utilizza rappresentazioni sollevate (lifted) basate sulla logica del primo ordine per garantire compattezza e generalità. Tuttavia, per essere risolti dai pianificatori basati su SAT (Soddisfacibilità Booleana), questi problemi devono spesso essere "groundati" (istantanziati completamente), ovvero trasformando tutte le azioni e i predicati in fatti specifici per ogni oggetto del dominio.

• Grounding Completo: Porta a un'esplosione esponenziale delle dimensioni del problema in domini con molti oggetti o predicati di alta arità, rendendo il ragionamento intrattabile.
• Grounding Assoluto (Lifted Puro): Approcci recenti come LiSAT operano direttamente a livello sollevato per evitare il grounding. Tuttavia, LiSAT presenta un limite critico: la dimensione della formula SAT cresce quadraticamente rispetto alla lunghezza del piano ($L$). Questo accade perché LiSAT non traccia esplicitamente lo stato, ma deve codificare collegamenti causali tra ogni azione e i suoi potenziali realizzatori in tutti i passaggi temporali precedenti. Questo limita la scalabilità per piani lunghi.

L'obiettivo del paper è trovare una "via di mezzo" che eviti sia l'esplosione esponenziale del grounding completo sia la crescita quadratica delle formule puramente sollevate.

2. Metodologia

Gli autori propongono un nuovo approccio di codifica SAT che mantiene le azioni completamente sollevate (utilizzando la tecnica degli Unified Arguments di LiSAT) ma grounda parzialmente la descrizione dello stato (i predicati).

Concetti Chiave:

• Gruppi di Mutex Sollevati (LMG) e Parzialmente Sollevati (PLMG): Sfruttano le invarianti del dominio (es. un pacchetto non può essere in due luoghi contemporaneamente). Un PLMG è un gruppo di mutex in cui alcune variabili sono già istanziate. Invece di generare tutti i fatti ground, si usa una rappresentazione compatta basata su variabili contate (counted variables) che indicano quale fatto del gruppo è vero.
• Codifica dello Stato Esplicita: A differenza di LiSAT, che usa collegamenti causali, le nuove codifiche tracciano esplicitamente lo stato a ogni passo temporale. Questo elimina la necessità di collegamenti causali quadratici, garantendo una crescita lineare della formula rispetto alla lunghezza del piano.

Le Tre Codifiche Proposte:

1. Grounding Completo (Fully Grounded): Grounda tutti i predicati. Funziona come baseline ma soffre dei problemi di scalabilità classici.
2. Grounding Parziale con Codifica One-Hot: Utilizza i PLMG per rappresentare gli stati. Per ogni gruppo di mutex, introduce variabili che indicano quale oggetto è associato a una variabile contata. Usa una codifica "one-hot" (una variabile booleana per ogni oggetto possibile).
3. Grounding Parziale con Codifica Binaria (Binary): Simile alla precedente, ma comprime la rappresentazione degli oggetti usando un numero logaritmico di bit ($\lceil \log_2 |O| \rceil$) invece di una variabile per oggetto. Questo riduce drasticamente il numero di variabili e clausole nei domini con molti oggetti.

Ottimizzazioni:

• Predicate Pruning (PP): Rimuove dai predicati groundati quelli che non appaiono né nelle precondizioni delle azioni né negli obiettivi, riducendo ulteriormente la dimensione della formula senza perdere informazioni rilevanti.

3. Contributi Chiave

1. Nuova Famiglia di Codifiche SAT: Introduzione di tre codifiche che combinano azioni sollevate e stati parzialmente groundati.
2. Scalabilità Lineare: La principale innovazione teorica è che la dimensione della formula scala linearmente con la lunghezza del piano ($O(L)$), risolvendo il collo di bottiglia quadratico ($O(L^2)$) di LiSAT.
3. Utilizzo Efficiente dei PLMG: Un metodo sistematico per selezionare e utilizzare i PLMG (tramite un approccio greedy) per comprimere la rappresentazione dello stato, gestendo sia mutex "al massimo uno" che "esattamente uno".
4. Codifica Binaria degli Oggetti: Applicazione della codifica binaria alle variabili di stato sollevate per ridurre la densità delle variabili nei problemi con grandi spazi di oggetti.

4. Risultati Sperimentali

Gli esperimenti sono stati condotti su benchmark standard di pianificazione sollevata (es. Blocksworld, Logistics, Rover, Visitall) confrontando le nuove codifiche con LiSAT (stato dell'arte per pianificazione ottima), Powerlifted (PWL), CPDDL e pianificatori groundati come Fast Downward e Madagascar.

• Pianificazione Ottima (Length-Optimal):
  • Le codifiche proposte (specialmente la versione Binary con Predicate Pruning) superano LiSAT in 5 domini su 9.
  • In domini difficili da groundare (come Logistics, Pipesworld, Rover), il miglioramento è significativo (≥20% di istanze risolte in più).
  • Le codifiche superano anche i metodi basati su ricerca (PWL, CPDDL) in termini di copertura totale, dimostrando che gli approcci basati su SAT sono competitivi o superiori per la pianificazione ottima.
• Pianificazione Satisficing (Sub-ottima):
  • Sebbene LiSAT e i metodi basati su ricerca (PWL) abbiano una copertura leggermente superiore in alcuni casi, le codifiche proposte offrono capacità complementari, risolvendo istanze che gli altri non riescono a gestire.
• Dimensione della Formula:
  • Le grafiche mostrano chiaramente che mentre LiSAT cresce quadraticamente (numero di variabili e clausole), le nuove codifiche crescono linearmente.
  • La codifica binaria riduce il numero di variabili fino a due ordini di grandezza rispetto alla codifica one-hot e a LiSAT in molti casi.

5. Significato e Conclusioni

Il paper dimostra che l'approccio "tutto o niente" (grounding completo o sollevamento completo) non è sempre ottimale. La grounding parziale rappresenta un punto di equilibrio efficace:

• Efficienza: Permette di gestire piani lunghi e domini complessi dove LiSAT fallisce a causa della crescita quadratica.
• Complessità: Mantiene la compattezza delle azioni sollevate, evitando l'esplosione esponenziale del grounding completo.
• Impatto: Offre un nuovo strumento per la pianificazione automatica, specialmente in scenari dove la lunghezza del piano è critica o il numero di oggetti è elevato.

Gli autori suggeriscono come lavoro futuro l'integrazione di parallelismo nelle azioni e il supporto per precondizioni negative ed effetti condizionali, ampliando ulteriormente l'applicabilità di queste codifiche parzialmente groundate.