Resumo Técnico: Além das Codificações Eager: Uma Abordagem Agnóstica à Teoria para Enumeração de Lemas Teóricos em SMT

1. Declaração do Problema

Em Satisfaibilidade Modulo Teorias (SMT), a elevação de técnicas de raciocínio booleano frequentemente requer a geração de lemas teóricos (T-lems). Estes são cláusulas T-válidas que eliminam atribuições de verdade que são proposicionalmente satisfatórias, mas T-inconsistentes.

Enquanto a resolução SMT padrão gera esses lemas de forma "preguiçosa" (lazy) sob demanda durante a busca, certas tarefas SMT complexas — como extração de núcleo de insatisfiabilidade mínima, MaxSMT e a compilação de T-OBDDs ou T-SDDs — exigem o pré-cálculo "eager" de um conjunto completo de T-lems antecipadamente.

As codificações "clássicas" eager SMT existentes são insuficientes para este propósito porque:

1. São específicas para poucas teorias simples (por exemplo, EUF, DL, LRA).
2. Não cumprem a combinação de teorias.
3. Frequentemente produzem números excessivos de lemas desnecessários.

Atualmente, há uma falta de métodos agnósticos à teoria para enumerar eficientemente conjuntos completos de T-lems para fórmulas arbitrárias, particularmente para aplicações de Compilação de Conhecimento (KC) onde o custo computacional é deslocado para uma fase offline, permitindo consultas online em tempo polinomial.

2. Metodologia

Os autores propõem um framework para enumerar T-lems que é agnóstico à teoria subjacente. A abordagem baseia-se em um método de linha de base usando AllSMT (enumerando todas as atribuições T-satisfatórias) e introduz três melhorias ortogonais e composáveis para aprimorar a escalabilidade:

2.1 Linha de Base: Enumeração Total AllSMT

O método de linha de base (Algoritmo 2) realiza uma enumeração AllSMT total, não projetada, na fórmula de entrada $\phi[\alpha]$. Ele encontra iterativamente atribuições de verdade totais T-satisfatórias, bloqueia-as e coleta os T-lems aprendidos pelo solucionador até que a fórmula se torne insatisfatória.

• Limitação: Esta abordagem depende da enumeração de atribuições totais. Como demonstrado no Exemplo 2, uma enumeração parcial ingênua pode falhar em gerar T-lems necessários porque o solucionador pode nunca explorar a atribuição total T-inconsistente específica que desencadeia um conflito. No entanto, enumerar todas as atribuições totais é frequentemente intratável computacionalmente devido à explosão combinatória.

2.2 Melhoria 1: Dividir e Conquistar (D&C)

Para mitigar o custo da enumeração total, os autores propõem uma estratégia de Dividir e Conquistar (Algoritmo 3):

1. Realizar uma enumeração AllSMT parcial para decompor o espaço de busca booleano em um conjunto de atribuições parciais disjuntas e T-satisfatórias ($M_{\alpha}^p$).
2. Para cada atribuição parcial $\mu \in M_{\alpha}^p$, realizar uma enumeração AllSMT total na fórmula restrita $\phi \land \mu$.
3. As enumerações totais são executadas em paralelo.

• Racional: Isso transforma uma única enumeração total grande e intratável em um passo de decomposição mais barato, mais muitos, mais gerenciáveis.

2.3 Melhoria 2: Enumeração Projetada

Os autores observam que a inconsistência T é determinada exclusivamente pela atribuição aos átomos teóricos ($\alpha_T$), e não aos átomos booleanos ($\alpha_B$).

• Método: Realizar enumeração AllSMT projetada apenas sobre $\alpha_T$ (Algoritmo 4).
• Base Teórica: O Teorema 1 prova que projetar a enumeração sobre átomos T produz um conjunto completo de T-lems.
• Benefício: Isso reduz drasticamente a dimensão da busca. Uma única atribuição T-satisfatória em $\alpha_T$ representa até $2^k$ atribuições totais no conjunto completo de átomos (onde $k$ é o número de átomos booleanos), reduzindo significativamente o uso de memória e o tamanho das cláusulas de bloqueio.

2.4 Melhoria 3: Particionamento Orientado à Teoria

Se o conjunto de átomos em $\phi$ puder ser particionado em conjuntos disjuntos ($\alpha_1, \dots, \alpha_n$) de modo que nenhum átomo em um conjunto compartilhe variáveis ou símbolos não interpretados com átomos em outro, o problema pode ser decomposto ainda mais (Algoritmo 5).

• Método: Com base na Propriedade 1 e no Teorema 2, os T-lems podem ser enumerados independentemente para cada partição. O algoritmo particiona iterativamente os átomos, enumera lemas para cada partição projetada sobre os átomos dessa partição e acumula os resultados.
• Benefício: Isso permite a decomposição de uma única enumeração total em $n$ enumerações projetadas independentes, oferecendo potenciais acelerações exponenciais para problemas com componentes disjuntos.

3. Contribuições Principais

1. Framework Agnóstico à Teoria: A primeira apresentação explícita de métodos para enumerar conjuntos completos de T-lems para teorias arbitrárias, indo além das codificações eager específicas de teoria.
2. Técnicas de Escalabilidade: A introdução de três técnicas ortogonais:
   • Dividir e Conquistar: Paraleliza a busca decompondo o espaço booleano.
   • Enumeração Projetada: Reduz a dimensionalidade da busca focando em átomos T.
   • Particionamento: Explora a disjunção estrutural na fórmula para resolver subproblemas independentemente.
3. Garantias Teóricas: Provas formais (Teoremas 1 e 2) demonstrando que essas otimizações preservam a completude do conjunto de T-lems necessária para eliminar todas as atribuições T-inconsistentes.
4. Integração com Compilação de Conhecimento: O trabalho serve como uma técnica habilitadora para elevar métodos de Compilação de Conhecimento (especificamente Diagramas de Decisão como OBDDs e SDDs) ao nível SMT, abordando o anterior gargalo da enumeração de T-lems.

4. Resultados Experimentais

As técnicas foram avaliadas em dois conjuntos de benchmarks:

• Instâncias sintéticas SMT(LRA): 450 problemas gerados aleatoriamente de [16].
• Instâncias de Planejamento Temporal: 90 codificações SMT de problemas de planejamento do domínio "Painter".

Métricas de Desempenho:

• Eficiência de Tempo:
  • Em benchmarks sintéticos, o D&C melhorou o desempenho em até 2 ordens de magnitude sobre a linha de base, resolvendo 17 problemas adicionais dentro do tempo limite.
  • Adicionar Projeção melhorou ainda mais os resultados, resolvendo 30 problemas a mais do que apenas o D&C e reduzindo drasticamente o tempo para instâncias previamente resolvidas.
  • Particionamento não mostrou melhoria em dados sintéticos (pois poucos problemas tinham partições disjuntas), mas foi altamente eficaz em problemas de planejamento.
  • Em problemas de planejamento, o Particionamento foi o fator dominante, permitindo a resolução de problemas com horizonte 5 que anteriormente eram intratáveis, alcançando acelerações de várias ordens de magnitude.
• Número de Lemas:
  • O D&C tendeu a produzir ligeiramente mais lemas devido à redundância paralela.
  • Projeção e Particionamento geralmente reduziram o número de lemas enumerados, mitigando a exploração redundante e gerando lemas mais fortes e menores.
• Tamanho do Lema:
  • O particionamento em problemas de planejamento resultou em T-lems significativamente menores (menos literais), provavelmente devido ao poda precoce de ramos T-inconsistentes envolvendo apenas partições específicas.

5. Significado e Alegações

O artigo afirma que essas técnicas aumentam drasticamente a eficiência e a escalabilidade da enumeração de T-lems em comparação com a abordagem AllSMT de linha de base.

• Papel Habilitador: O significado principal é permitir a aplicação prática da Compilação de Conhecimento ao SMT. Os autores observam que, em seu trabalho anterior [16], a enumeração de T-lems era o "principal gargalo" para compilar Diagramas de Decisão. Ao resolver esse gargalo, os métodos propostos abrem caminho para escalar essas técnicas de compilação para instâncias complexas e do mundo real.
• Modéstia: Os autores têm o cuidado de notar que as melhorias dependem do contexto. Por exemplo, a projeção não ajudou com problemas de planejamento porque as atribuições de átomos T eram consequências determinísticas de atribuições booleanas nessas codificações específicas. Da mesma forma, o particionamento só gerou benefícios quando a estrutura do problema permitia naturalmente partições disjuntas.

Em resumo, o artigo fornece um toolkit robusto e agnóstico à teoria para enumeração eager de T-lems, transformando uma etapa anteriormente intratável em um processo escalável, facilitando assim aplicações SMT avançadas como MaxSMT e Compilação de Conhecimento.