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

Este artigo apresenta três codificações SAT para planejamento que mantêm as ações no nível levantado enquanto aplicam uma grounding parcial aos predicados, alcançando uma escalabilidade linear em relação ao comprimento do plano e superando o estado da arte em domínios difíceis de groundar.

O essencial

Imagine que você é um chefe de cozinha tentando organizar um banquete gigante para 1.000 pessoas.

O seu problema é o seguinte: você tem um livro de receitas (o plano) e uma despensa cheia de ingredientes (os objetos e ações). O objetivo é descobrir a sequência exata de passos para transformar os ingredientes crus em pratos prontos, sem errar.

O Problema: A "Explosão" da Lista de Compras

Na inteligência artificial, os computadores tentam fazer isso de duas formas principais:

1. A Abordagem "Tudo no Chão" (Grounding): O computador pega cada ingrediente individualmente. Se você tem 1.000 pessoas e 5 tipos de pratos, ele cria uma lista de 5.000 tarefas específicas: "Cozinhar o prato 1 para a pessoa A", "Cozinhar o prato 1 para a pessoa B", etc.

   • O problema: A lista fica tão grande que o computador fica sobrecarregado, como se tentasse ler um livro de telefone inteiro para decidir o que fazer. Isso é chamado de "explosão exponencial".

2. A Abordagem "Super Abstrata" (Lifted): O computador tenta ser inteligente e diz: "Não vou listar cada pessoa. Vou apenas dizer 'Cozinhar o prato 1 para QUALQUER pessoa'".

   • O problema: Embora a lista seja curta, a lógica para verificar se isso funciona em cada momento do tempo fica muito complexa. É como tentar resolver um quebra-cabeça onde as peças mudam de lugar a cada segundo. O método atual mais famoso (chamado LiSAT) funciona bem para cozinhas pequenas, mas quando o tempo do banquete aumenta (planos longos), a complexidade cresce de forma quadrática (se o tempo dobra, o trabalho quadruplica).

A Solução: O "Meio-Termo" Inteligente

Os autores deste artigo (João Filipe e Gregor Behnke) propuseram uma solução criativa: o "Meio-Termo".

Eles criaram um sistema que mistura o melhor dos dois mundos:

• As Ações continuam Abstratas: O computador ainda pensa em termos gerais ("Cozinhar para qualquer pessoa"). Isso mantém a lista de tarefas curta.
• O Estado é Parcialmente Concreto: Em vez de tentar ser 100% abstrato sobre onde os ingredientes estão, eles usam um truque chamado Grupos de Mutex Levantados (PLMGs).

A Analogia do "Grupo de Amigos"

Imagine que você tem um grupo de amigos. Você sabe uma regra: "Neste grupo, apenas uma pessoa pode estar na sala de estar a qualquer momento".

• O jeito antigo (Grounding): O computador verificaria: "A Maria está na sala? O João está na sala? A Ana está na sala?" (1.000 verificações).
• O jeito novo (PLMG): O computador diz: "Ok, existe um 'Grupo da Sala de Estar'. Apenas um deles está lá. Eu só preciso de um botão para dizer 'Quem é o escolhido?'".

Isso permite que o computador ignore a maioria das combinações impossíveis e foque apenas no que importa.

O Truque da "Codificação Binária" (O Código de Barras)

Para tornar isso ainda mais rápido, eles usaram uma técnica de codificação binária.

• Imagine que, em vez de escrever o nome de cada pessoa em um papel (o que ocupa muito espaço), você dá a cada pessoa um número de código de barras (ex: 001, 010, 011).
• Com apenas alguns bits (0s e 1s), você consegue representar milhares de pessoas.
• Isso reduz drasticamente o tamanho da "lista de verificação" que o computador precisa processar.

O Resultado: Mais Rápido e Mais Longo

Os autores testaram essa ideia em vários cenários difíceis (como logística de caminhões, robôs explorando planetas e labirintos).

• O que eles descobriram: O novo método cresce de forma linear. Se você dobrar o tamanho do banquete (o tempo do plano), o trabalho do computador apenas dobra.
• Comparação: O método antigo (LiSAT) cresce de forma quadrática. Se você dobrar o tempo, o trabalho quadruplica. Em planos longos, o novo método é muito mais rápido.
• Desempenho: Em 5 dos 9 testes difíceis, o novo método venceu o atual campeão (LiSAT), especialmente em domínios onde é difícil "aterrissar" (ground) todos os detalhes.

Resumo em uma Frase

Os autores criaram um novo jeito de planejar para robôs e softwares que, em vez de listar cada detalhe minúsculo ou tentar ser super abstrato, usa "atalhos lógicos" (como grupos de amigos e códigos binários) para resolver problemas complexos de forma muito mais eficiente e rápida, especialmente quando o plano precisa ser longo.

É como trocar uma lista de compras de 10.000 itens por um código de barras inteligente que o computador consegue ler instantaneamente, sem precisar verificar cada item um por um.

Resumo técnico

Resumo Técnico: Codificação Parcialmente Aterada de Planejamento para SAT

1. O Problema

O planejamento automático clássico lida com problemas definidos em representações de primeira ordem "elevadas" (lifted), que oferecem compactação e generalidade. No entanto, a maioria dos planejadores converte (ground) essas representações para instâncias concretas para facilitar o raciocínio.

• Grounding Total: Causa uma explosão exponencial no tamanho do problema em domínios complexos ou com muitos objetos, limitando a escalabilidade.
• Planejamento Totalmente Elevado (Lifted): Abordagens recentes, como LiSAT (Höller e Behnke, 2022), operam diretamente no nível elevado para evitar o grounding completo. No entanto, LiSAT apresenta uma limitação crítica: o tamanho da fórmula SAT cresce quadraticamente com o comprimento do plano ($L$). Isso ocorre porque LiSAT utiliza "links causais" para garantir que pré-condições sejam atendidas sem rastrear explicitamente o estado, o que se torna ineficiente para planos longos.

O objetivo deste trabalho é encontrar um "meio-termo" entre o grounding total e o totalmente elevado, criando uma codificação que mantenha a escalabilidade linear em relação ao comprimento do plano.

2. Metodologia

Os autores propõem três novas codificações SAT que mantêm as ações totalmente elevadas (usando a técnica de "Argumentos Unificados" do LiSAT) mas parcialmente ateram a descrição do estado (predicados).

A abordagem central baseia-se em Grupos de Mutex Parcialmente Elevados (PLMGs - Partially Lifted Mutex Groups).

• Conceito de PLMG: Em vez de listar todos os fatos possíveis (ex: at(p1, l1), at(p1, l2)...), o sistema identifica grupos de fatos mutuamente exclusivos (ex: um pacote só pode estar em um lugar por vez). Um PLMG usa variáveis contadas (counted variables) para representar implicitamente qual fato do grupo está verdadeiro, sem precisar gerar todas as instâncias concretas.
• Codificação do Estado: O estado é representado explicitamente ao longo do tempo (diferente do LiSAT, que é "stateless"). Isso elimina a necessidade de links causais complexos, permitindo um crescimento linear da fórmula.

As três codificações propostas:

1. Grounding Total (Baseline): Ateram todos os predicados. Serve como comparação, mas sofre com a explosão de tamanho em domínios grandes.
2. Grounding Parcial (One-Hot): Usa PLMGs para representar predicados. Para cada variável contada, utiliza uma codificação one-hot (uma variável booleana por objeto possível).
3. Grounding Parcial (Binária): Uma otimização da anterior. Em vez de uma variável por objeto, utiliza uma representação binária ($\lceil \log_2 |O| \rceil$ variáveis) para codificar o valor das variáveis contadas. Isso aumenta a densidade de informação e reduz o número total de variáveis e cláusulas, especialmente em problemas com muitos objetos.

Otimizações Adicionais:

• Poda de Predicados (Predicate Pruning): Remove predicados que não aparecem em pré-condições ou no objetivo, reduzindo o espaço de busca.
• Axiomas de Quadro (Frame Axioms): Garantem que o estado só muda se uma ação causar a mudança, utilizando variáveis de causa para rastrear alterações nas variáveis contadas dos PLMGs.

3. Contribuições Principais

• Escalabilidade Linear: A principal contribuição teórica é demonstrar que é possível codificar planejamento SAT com crescimento linear em relação ao comprimento do plano ($O(L)$), superando a limitação quadrática ($O(L^2)$) do LiSAT.
• Novas Codificações Híbridas: Introdução de codificações que combinam a compactação das ações elevadas com a eficiência da representação de estado baseada em PLMGs.
• Codificação Binária de Objetos: Adaptação de técnicas de representação binária para variáveis contadas em PLMGs, reduzindo significativamente o número de variáveis em problemas com grandes conjuntos de objetos.
• Desempenho Empírico: Demonstração de que essa abordagem supera o estado da arte (LiSAT) em domínios difíceis de aterar (hard-to-ground).

4. Resultados Experimentais

Os experimentos foram realizados em benchmarks padrão de planejamento elevado, comparando as novas codificações com LiSAT, planejadores baseados em busca (Powerlifted, CPDDL) e planejadores aterados (Madagascar, Fast Downward).

• Planejamento de Comprimento Ótimo (Optimal):
  • As codificações propostas (especialmente a versão Binária com Poda) superaram o LiSAT em 5 dos 9 domínios de benchmark.
  • Em domínios como Logistics, Pipesworld e Rover, houve melhorias de mais de 20% no número de instâncias resolvidas.
  • O crescimento linear permitiu resolver planos mais longos onde o LiSAT falhava devido ao tamanho excessivo da fórmula.
• Planejamento Satisficing:
  • Embora o LiSAT e métodos baseados em busca tenham cobertura ligeiramente superior em alguns domínios devido a heurísticas específicas, as codificações SAT propostas mostraram capacidades complementares, resolvendo problemas que os planejadores baseados em busca não conseguiam.
• Tamanho da Fórmula:
  • Variáveis: A codificação Binária Parcialmente Aterada (Binary PP) geralmente usa menos variáveis que o LiSAT (até duas ordens de magnitude em alguns casos).
  • Cláusulas: A codificação gera mais cláusulas que o LiSAT (devido à complexidade de codificar a semântica dos PLMGs), mas o crescimento é linear, enquanto o do LiSAT é quadrático. Em planos longos, a vantagem linear torna-se decisiva.
• Tempo de Execução: Não há dominância clara entre LiSAT e a nova abordagem; o desempenho depende do domínio. Isso sugere que as abordagens são ortogonais e poderiam ser usadas em conjunto em um portfólio de planejadores.

5. Significado e Conclusão

Este trabalho resolve um dilema fundamental no planejamento baseado em SAT: a escolha entre a explosão de tamanho do grounding total e a ineficiência quadrática do planejamento totalmente elevado para planos longos.

Ao introduzir o conceito de codificação parcialmente aterada, os autores demonstram que é possível manter a generalidade das representações elevadas para as ações enquanto se utiliza estruturas de invariantes (PLMGs) para compactar a representação do estado. O resultado é um método que escala linearmente, tornando viável o planejamento ótimo em domínios complexos e de grande escala que eram anteriormente intratáveis para planejadores SAT puros.

A pesquisa abre caminho para futuras extensões, como a integração de paralelismo de ações e suporte a pré-condições negativas e efeitos condicionais, consolidando o SAT como uma ferramenta robusta para planejamento elevado.