Resumo Técnico: Enumeração Projetada Disjunta para SAT e SMT sem Cláusulas de Bloqueio

Declaração do Problema

O artigo aborda os desafios computacionais inerentes à Satisfatibilidade de Todas as Soluções (AllSAT) e sua extensão, Satisfatibilidade de Todas as Soluções Modulo Teorias (AllSMT). O objetivo é enumerar todas as atribuições satisfatórias de uma fórmula. Enquanto a resolução SAT tradicional termina ao encontrar uma única solução, a enumeração requer a exploração de todo o espaço de busca.

Duas dificuldades principais são identificadas:

1. Espaço de Busca Exponencial: Para uma fórmula com $n$ variáveis, existem $2^n$ atribuições totais possíveis. A enumeração explícita é inviável para $n$ grande. O artigo defende o uso de atribuições parciais (implicantes) para representar conjuntos de atribuições totais, comprimindo assim o espaço de soluções.
2. Cláusulas de Bloqueio e Memória: Solvers AllSAT tradicionais baseados em Aprendizado de Cláusulas por Conflito Dirigido (CDCL) e Retrocesso Não Cronológico (NCB) dependem da adição de cláusulas de bloqueio para impedir a re-descoberta do mesmo modelo. À medida que o número de modelos cresce, o número de cláusulas de bloqueio pode tornar-se exponencial, levando a explosões de memória e desempenho degradado na propagação unitária.
3. Projeção: Em muitas aplicações (por exemplo, converter fórmulas não-CNF via transformação de Tseitin), é necessário enumerar soluções apenas para um subconjunto de variáveis "importantes" ($V_r$), ignorando variáveis auxiliares "irrelevantes" ($V_i$).

O artigo foca na enumeração disjunta, onde atribuições repetidas são estritamente proibidas, um requisito para aplicações como Integração de Modelos Ponderados (WMI) e inferência probabilística.

Metodologia

Os autores propõem dois solvers inovadores: TabularAllSAT (para lógica proposicional) e TabularAllSMT (para SMT). Ambos integram CDCL com Retrocesso Cronológico (CB) para eliminar a necessidade de cláusulas de bloqueio, mantendo a disjunção.

1. Algoritmo Central de Busca (CDCL + CB)

O loop de busca combina as forças do CDCL (escapar de regiões insatisfatíveis via análise de conflito) e do CB (exploração sistemática sem cláusulas de bloqueio redundantes).

• Tratamento de Conflito: Quando um conflito é detectado, o solver realiza a análise padrão de conflito para derivar uma cláusula de conflito. No entanto, em vez de retroceder não cronologicamente para o nível da cláusula de conflito (como no CDCL padrão), o solver retrocede cronologicamente para o literal de decisão mais recentemente atribuído e inverte seu valor.
• Bloqueio Implícito: Para garantir a disjunção sem armazenar cláusulas de bloqueio explícitas, o solver utiliza cláusulas de razão de retrocesso virtuais. Quando um modelo é encontrado e um literal de decisão é invertido, a razão para a inversão é registrada como Backtrue. Isso define implicitamente uma cláusula de bloqueio consistindo na negação de todos os literais de decisão até aquele ponto.
• Terminação: A busca termina quando o solver retrocede ao nível de decisão 0, garantindo que todo o espaço tenha sido escaneado sistematicamente sem repetição.

2. Redução Cronológica de Implicantes

Um componente crítico é a redução de atribuições totais em atribuições parciais compactas (implicantes). O artigo introduz dois algoritmos:

• Redução Conservadora (Linha de Base): Baseada em literais vigiados 2, este algoritmo verifica se um literal é necessário para que a atribuição parcial atual satisfaça a fórmula. Ele respeita a ordem de decisão e as flags Backtrue para garantir a disjunção.
• Redução Agressiva (Novo): Este algoritmo simula uma ordenação de decisão ótima. Ele identifica literais "necessários" (aqueles requeridos para satisfazer cláusulas específicas) e literais "desnecessários". Ele permite a remoção de literais desnecessários independentemente de seu nível de decisão, desde que não estejam marcados com Backtrue ou envolvidos na análise de conflito. Isso é alcançado por:
  1. Contar quantos literais em cada cláusula estão atualmente no rastro.
  2. Remover iterativamente literais que não são o único satisfator de qualquer cláusula.
  3. Reconstruir o rastro apenas com os literais necessários, efetivamente adiando a atribuição de variáveis desnecessárias para o final do loop de busca.

3. Extensões para Projeção e SMT

• Enumeração Projetada: O algoritmo é adaptado para lidar com um subconjunto de variáveis relevantes ($V_r$). A heurística de decisão prioriza $V_r$ sobre variáveis irrelevantes ($V_i$). Durante a redução de implicantes, literais correspondentes a $V_i$ são automaticamente descartados, garantindo que a saída contenha apenas atribuições para $V_r$.
• Integração AllSMT: O framework integra um solver de teoria (MathSAT5). O loop de busca inclui uma verificação de consistência-T após a propagação unitária. Se um conflito de teoria surgir, ele é analisado de forma semelhante a um conflito booleano, e o solver retrocede cronologicamente. Átomos de teoria gerados durante a resolução são tratados como variáveis irrelevantes para fins de projeção.

Contribuições Principais

O artigo delineia cinco contribuições principais:

1. Enumeração Parcial Disjunta: Um procedimento combinando CDCL e Retrocesso Cronológico para enumerar modelos parciais disjuntos sem introduzir cláusulas de bloqueio.
2. Algoritmos de Redução de Implicantes: Dois algoritmos (conservador e agressivo) projetados para minimizar atribuições parciais enquanto aderem estritamente às restrições de disjunção do cálculo subjacente.
3. Extensão de Enumeração Projetada: Adaptação do solver para enumerar apenas um subconjunto de variáveis importantes, lidando com variáveis auxiliares introduzidas durante a transformação CNF.
4. Extensão SMT: Integração de raciocínio de teoria no framework de enumeração, permitindo a resolução AllSMT com enumeração parcial disjunta.
5. Avaliação Experimental: Um benchmark abrangente contra solvers de última geração.

Resultados Experimentais

Os autores avaliaram TabularAllSAT e TabularAllSMT em vários benchmarks (3-SAT aleatório, SATLIB, SMT sintético e fórmulas não-CNF) contra solvers incluindo MathSAT5, Dualiza, solvers baseados em BDD e D4+ModelGraph.

• Redução de Implicantes: O novo algoritmo de redução agressiva reduziu significativamente o número de atribuições parciais geradas em comparação com a linha de base conservadora, particularmente em instâncias com um alto número de soluções totais. Embora tenha incorrido em uma pequena sobrecarga em instâncias muito pequenas, melhorou o tempo de execução geral em problemas maiores.
• Desempenho AllSAT: O TabularAllSAT desempenhou de forma competitiva ou superior à maioria dos solvers (BC, NBC, MathSAT5). Foi superado por ferramentas de compilação de conhecimento (BDD, D4+ModelGraph) em benchmarks específicos com poucas cláusulas onde a sobrecarga de compilação era baixa. No entanto, o TabularAllSAT demonstrou uma pegada de memória menor e não experimentou tempos limite devido à exaustão de memória.
• AllSAT Projetado: Em benchmarks não-CNF que exigem projeção, o TabularAllSAT superou significativamente o MathSAT5 e o Dualiza tanto em velocidade quanto no número de instâncias resolvidas. Também superou o D4+ModelGraph em benchmarks sintéticos mais difíceis.
• Desempenho AllSMT: O TabularAllSMT superou o MathSAT5 (o único outro solver AllSMT projetado publicamente disponível) em tarefas de enumeração total e enumeração parcial. A ausência de cláusulas de bloqueio no TabularAllSMT impediu a degradação de desempenho observada no MathSAT5 à medida que a complexidade do problema aumentava.

Significado e Alegações

O artigo alega que a abordagem proposta oferece uma alternativa superior à enumeração tradicional baseada em cláusulas de bloqueio, particularmente em cenários que exigem projeção e raciocínio SMT.

• Eficiência: Ao evitar o crescimento exponencial das cláusulas de bloqueio, o solver mantém um desempenho estável de propagação unitária e evita explosões de memória.
• Compactação: O algoritmo agressivo de redução de implicantes produz atribuições parciais mais compactas, reduzindo o tamanho da saída e o espaço de busca para etapas subsequentes de enumeração.
• Generalidade: O framework unifica com sucesso CDCL e Retrocesso Cronológico tanto para enumeração proposicional quanto baseada em teoria, estendendo a aplicabilidade da enumeração disjunta a domínios complexos como inferência probabilística e contagem de modelos sobre teorias de primeira ordem.

Os autores posicionam seu trabalho como uma realização prática do cálculo formal apresentado em [17], fornecendo a primeira implementação que lida efetivamente com projeção e SMT sem a sobrecarga de cláusulas de bloqueio.