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

Este artículo presenta tres codificaciones SAT que logran un equilibrio entre la representación totalmente levantada y totalmente instanciada mediante la mantención de acciones levantadas y la instanciación parcial de predicados, logrando una escalabilidad lineal en la longitud del plan y superando al estado del arte en dominios difíciles de instanciar.

Lo esencial

Imagina que estás organizando un viaje para un grupo enorme de amigos. Tienes que decidir quién se sienta en qué coche, quién lleva qué maleta y qué ruta tomarán.

El problema es que, si intentas hacer una lista completa y detallada de todas las posibilidades desde el principio (por ejemplo: "Juan en el coche A con la maleta roja", "Juan en el coche B con la maleta roja", "María en el coche A...", etc.), la lista se vuelve tan gigantesca que tu cerebro (o una computadora) se agota antes de empezar a pensar. Esto es lo que pasa en la planificación automática cuando se intenta "aterrizar" (grounding) todo el problema: se crean demasiados casos específicos.

Por otro lado, si intentas pensar solo en reglas generales sin nombres ("Alguien va en algún coche"), es muy flexible, pero a veces es tan abstracto que es difícil encontrar una solución concreta y rápida.

La idea central del papel: El "Justo Medio"

Este artículo presenta una nueva forma de pensar que se sitúa en el punto medio entre la lista gigante y la regla abstracta. Los autores llaman a esto una "codificación parcialmente aterrizada".

Aquí tienes la analogía para entenderlo:

1. El problema de los "Planos de Vuelo" (LiSAT)

Imagina que el método anterior más famoso (llamado LiSAT) es como un controlador de tráfico aéreo que no tiene una lista de aviones, sino que solo sabe las reglas: "Si un avión despega, otro debe aterrizar".

• Ventaja: Es muy flexible y maneja muchos aviones.
• Desventaja: Para saber si el vuelo de mañana es posible, tiene que revisar todas las posibles conexiones entre todos los aviones de todos los días. Si el viaje es largo (muchos días), el trabajo crece de forma explosiva (cuadráticamente). Es como intentar adivinar el futuro conectando cada punto con cada otro punto; se vuelve imposible para viajes largos.

2. La solución de los autores: "Etiquetas de Maleta" (Codificación Parcial)

Los autores proponen una nueva estrategia. Imagina que en lugar de escribir una lista de quién va en qué coche, usas etiquetas inteligentes:

• Mantienes las acciones (como "conducir", "cargar maleta") en un formato general y flexible (nadie tiene nombre propio todavía).
• Pero para el estado (dónde están las cosas), usas un sistema de "grupos de mutex" (grupos de exclusión mutua).

La analogía de la "Caja de Herramientas":
Imagina que tienes una caja de herramientas.

• Método antiguo (Aterrizado completo): Escribes en un papel: "El martillo está en la caja 1", "El destornillador en la caja 2", "El martillo en la caja 3"... hasta agotar todas las cajas. Si tienes 1000 cajas, tienes 1000 papeles.
• Método LiSAT: Solo dices "Hay una herramienta en alguna caja", pero para verificarlo, tienes que mirar todas las cajas de todas las cajas anteriores.
• El nuevo método (Parcialmente aterrizado): Dices: "Solo hay una herramienta en la caja de 'martillos'". Usas una etiqueta que dice "Martillo". No necesitas saber exactamente en qué caja está el martillo hasta que sea necesario. Si el martillo se mueve, solo actualizas la etiqueta "Martillo -> Caja 5".

¿Por qué es mejor?

1. Escalabilidad Lineal vs. Cuadrática:

   • Piensa en el método antiguo como subir una escalera donde cada paso requiere que revises todos los pasos anteriores. Si la escalera es larga, tardas una eternidad.
   • El nuevo método es como subir una escalera donde solo revisas el paso anterior. Si la escalera es el doble de larga, tardas el doble de tiempo (lineal), no cuatro veces más. Esto es crucial para planes largos.

2. Aprovechar la Estructura:
   El método usa "grupos de mutex" (LMGs). Es como decir: "Un paquete no puede estar en dos lugares a la vez". En lugar de verificar cada paquete individualmente contra cada lugar, el sistema sabe que, por definición, si el paquete A está en Madrid, no puede estar en París. Esto elimina millones de posibilidades inútiles de la lista de verificación.

El resultado en la vida real

Los autores probaron su método en problemas difíciles (como logística, transporte de paquetes, laberintos).

• En problemas largos y difíciles: Su nuevo método (especialmente la versión con "codificación binaria", que es como usar código binario para guardar información en lugar de escribirlo todo en letras) ganó a los mejores métodos anteriores.
• En problemas cortos: A veces es un poco más lento, pero sigue siendo muy competitivo.

En resumen

Imagina que tienes que organizar un banquete para 10.000 personas.

• El método viejo: Haces una lista de 10.000 nombres y 10.000 platos, y luego intentas combinar cada nombre con cada plato para ver qué funciona. Se vuelve un caos.
• El método LiSAT: Intentas adivinar las combinaciones sin lista, pero revisando cada posible historia pasada. Se vuelve lento si el banquete dura muchos días.
• El nuevo método: Creas grupos. "Todos los niños comen pizza", "Todos los adultos comen ensalada". Usas etiquetas para mover los grupos. Si un niño quiere cambiar de mesa, solo mueves la etiqueta del grupo "Niños".

Conclusión: Los autores han encontrado una forma inteligente de planificar que no se ahoga en detalles innecesarios, permitiendo resolver problemas mucho más grandes y complejos que antes eran imposibles para las computadoras. Es como pasar de contar cada grano de arena de una playa a contar solo los montones de arena.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo en español:

Título

Cuando tanto Grounding (Instanciación) como no Grounding son Malos: Una Codificación Parcialmente Grounded de la Planificación a SAT

1. El Problema

La planificación automática clásica suele definirse mediante representaciones de primer orden "levantadas" (lifted), que son compactas y generales. Sin embargo, la mayoría de los planificadores convierten (ground) estas representaciones a instancias concretas para facilitar el razonamiento, lo que a menudo provoca un estallido exponencial en el tamaño del problema, especialmente en dominios con muchos objetos.

Las aproximaciones recientes intentan operar directamente en el nivel levantado para evitar este grounding completo. Un enfoque destacado es LiSAT (Holler y Behnke, 2022), que utiliza una codificación totalmente levantada sin rastrear el estado explícitamente, sino mediante enlaces causales. Aunque LiSAT es el estado del arte para planificación óptima en longitud, tiene una limitación crítica:

• Escalabilidad Cuadrática: El tamaño de la fórmula SAT crece cuadráticamente con la longitud del plan ($\ell$) debido a la necesidad de codificar enlaces causales entre cada precondición y sus posibles realizadores en pasos anteriores. Esto limita su escalabilidad en problemas que requieren planes largos.
• Incapacidad para explotar estructuras: LiSAT no puede aprovechar estructuras inherentes como los grupos de mutex levantados (LMGs) de manera eficiente.

2. Metodología

Los autores proponen un "punto medio" entre la planificación totalmente levantada y totalmente grounded. Introducen tres codificaciones SAT que mantienen las acciones completamente levantadas pero groundan parcial o totalmente los predicados (el estado).

Conceptos Clave:

• Acciones Levantadas: Se utiliza la técnica de "Argumentos Unificados" (Unified Arguments) de LiSAT, donde los argumentos de las acciones se comparten basándose en sus tipos, no en su posición, manteniendo la representación compacta de las acciones.
• Grounding Parcial del Estado: En lugar de groundear todos los hechos o mantener el estado totalmente levantado, se utiliza una representación híbrida:
  1. Grounding Total (Baseline): Groundear todos los predicados (similar a planificadores SAT clásicos).
  2. Grounding Parcial con PLMGs: Utilizar Grupos de Mutex Parcialmente Levantados (PLMGs). Un PLMG permite representar un conjunto de hechos donde, en cualquier estado alcanzable, máximo uno (o exactamente uno) es verdadero. En lugar de generar variables para cada hecho, se usan variables contadas para denotar cuál de los hechos del grupo está activo.
  3. Codificación Binaria: Para mejorar la densidad de información en los PLMGs, se propone una codificación binaria de los objetos en lugar de una codificación "one-hot", reduciendo el número de variables necesarias de $O(|O|)$ a $O(\log |O|)$.

Mecanismo de Codificación:

• Crecimiento Lineal: Al rastrear el estado explícitamente (mediante variables de hechos o PLMGs) en lugar de usar enlaces causales, se elimina la necesidad de la cuadrática. El tamaño de la fórmula escala linealmente con la longitud del plan ($\ell$).
• Axiomas de Marco (Frame Axioms): Se implementan axiomas de marco para asegurar que el estado solo cambia si una acción lo modifica, utilizando variables de causa para rastrear los cambios en las variables contadas de los PLMGs.
• Poda de Predicados (Predicate Pruning): Se eliminan predicados que no aparecen en precondiciones ni en el objetivo, reduciendo significativamente el número de hechos a codificar.

3. Contribuciones Clave

1. Nuevas Codificaciones SAT: Presentación de tres esquemas de codificación que combinan acciones levantadas con estados parcialmente grounded.
2. Escalabilidad Lineal: Demostración teórica y práctica de que el tamaño de la fórmula crece linealmente con la longitud del plan, superando la limitación cuadrática de LiSAT.
3. Uso de PLMGs: Aplicación efectiva de Grupos de Mutex Parcialmente Levantados para comprimir la representación del estado, permitiendo manejar dominios con muchos objetos sin explotar exponencialmente.
4. Codificación Binaria de Objetos: Una variante que reduce el número de variables mediante representación binaria, mejorando la eficiencia en problemas con grandes espacios de objetos.
5. Evaluación Empírica: Comparación exhaustiva contra el estado del arte (LiSAT, Powerlifted, CPDDL) y planificadores grounded (Madagascar, Fast Downward).

4. Resultados Experimentales

Los experimentos se realizaron en el conjunto de benchmarks estándar para planificación levantada, utilizando el solver SAT Kissat.

• Planificación Óptima (Longitud Óptima):
  • Las codificaciones propuestas (especialmente la versión "Binary" con poda de predicados) superan a LiSAT en 5 de los 9 dominios de prueba.
  • En dominios difíciles de groundear (como Logistics, Pipesworld y Rover), la mejora es significativa (≥20% más de instancias resueltas).
  • En general, los métodos basados en SAT (incluyendo los nuevos y LiSAT) superan a los métodos basados en búsqueda (Powerlifted, CPDDL) en este modo.
• Planificación Satisficing (Subóptima):
  • El enfoque propuesto es competitivo, mostrando capacidades complementarias a los planificadores basados en búsqueda. Resuelve instancias en dominios como Blocksworld, Childsnack y Visitall donde otros planificadores levantados fallan.
• Tamaño de la Fórmula:
  • Aunque la codificación propuesta genera más cláusulas que LiSAT en algunos casos (debido a la complejidad de codificar la semántica de los PLMGs), el número de variables es significativamente menor (hasta dos órdenes de magnitud en algunos casos).
  • La gráfica de crecimiento confirma la tendencia lineal de las nuevas codificaciones frente a la tendencia cuadrática de LiSAT.
• Tiempo de Ejecución:
  • No hay un dominio claro de superioridad absoluta; el rendimiento depende del dominio. Esto sugiere que los enfoques tienen capacidades ortogonales, siendo ideales para un planificador de cartera (portfolio).

5. Significado e Impacto

Este trabajo es fundamental porque resuelve el dilema de la escalabilidad en la planificación basada en SAT:

• Rompe la barrera cuadrática: Permite resolver problemas con planes más largos que LiSAT, algo que antes era prohibitivo debido al tamaño de la fórmula.
• Equilibrio óptimo: Demuestra que no es necesario elegir entre "totalmente levantado" (compacto pero difícil de razonar) y "totalmente grounded" (fácil de razonar pero explosivo). La vía intermedia (acciones levantadas + estado parcialmente grounded) ofrece el mejor de los dos mundos.
• Complementariedad: Proporciona herramientas que cubren las debilidades de los planificadores basados en búsqueda actuales, sugiriendo que el futuro de la planificación eficiente podría residir en la combinación de estas técnicas.

En conclusión, los autores presentan una evolución necesaria en la planificación SAT, logrando un rendimiento superior en la planificación óptima de longitud en dominios complejos y estableciendo una nueva línea base para la escalabilidad en problemas de planificación levantada.