WME: Extending CDCL-based Model Enumeration with Weights

Este trabalho apresenta algoritmos baseados em CDCL para Enumeração de Modelos Ponderados (WME), integrando propagação, poda e análise de conflitos ponderados em frameworks de retrocesso cronológico e não cronológico para permitir consultas orientadas por pesos, como a enumeração dos k melhores modelos.

O essencial

Imagine que você é um detetive em uma cidade gigante chamada "Lógica". Sua missão é encontrar todas as casas (soluções) onde as regras da cidade são respeitadas.

Até agora, os detetives tradicionais (os softwares de lógica) tinham dois modos de trabalho principais:

1. O "Contador de Casas" (AllSAT): Eles encontravam todas as casas, uma por uma, sem se importar se a casa era um castelo de ouro ou uma cabana de palha. Eles apenas listavam tudo.
2. O "Caçador de Tesouros" (MaxSAT): Eles só queriam encontrar a única casa mais valiosa da cidade e paravam assim que a achavam.

O problema é que, na vida real (como em diagnósticos médicos ou inteligência artificial), muitas vezes queremos algo no meio do caminho: "Me mostre as 10 melhores casas, ou me mostre todas as casas que valem mais de 1 milhão de dólares."

Os métodos antigos não faziam isso bem. Ou eles gastavam tempo demais listando casas ruins, ou só encontravam a melhor e ignoravam as outras boas.

A Grande Ideia: WME (Enumeração de Modelos com Pesos)

Os autores deste artigo criaram um novo tipo de detetive chamado WME. A grande inovação é que esse detetive carrega uma balança mágica e um mapa de tesouros.

Aqui está como funciona, usando analogias simples:

1. A Balança Mágica (Propagação de Peso)

Imagine que cada porta que você abre em uma casa tem um peso. Algumas portas levam a quartos dourados (peso alto), outras a porões escuros (peso baixo).
O detetive WME não espera chegar ao fim da casa para saber quanto ela vale. Ele calcula o valor enquanto caminha.

• O Truque: Se o detetive entra em um corredor e percebe que, mesmo que ele encontre todos os tesouros restantes, o valor total nunca vai atingir a meta (digamos, 1 milhão), ele para imediatamente. Ele não perde tempo explorando aquele corredor. Isso é chamado de "poda" (cortar o caminho inútil).

2. O Mapa de "Não Volte Aqui" (Análise de Conflito)

Quando o detetive percebe que um caminho é inútil, ele não apenas desiste. Ele escreve um bilhete no mapa: "Se você vir a porta A e a porta B abertas, nunca tente entrar aqui de novo, porque não há tesouro."
Isso ajuda o detetive a não cometer o mesmo erro duas vezes, tornando a busca muito mais rápida.

3. Dois Estilos de Detetive (Backtracking)

Os autores testaram duas formas de o detetive se mover quando ele se perde ou precisa recuar:

• Estilo "Passo a Passo" (Backtracking Cronológico):

  • Como funciona: Se o detetive se perde, ele volta exatamente um passo, como se estivesse caminhando de volta pela mesma trilha.
  • Vantagem: É muito leve, não precisa de muita memória (como uma mochila pequena).
  • Melhor para: Quando há muitas casas boas para encontrar (como listar todas as casas acima de um certo valor). Ele é eficiente em encontrar volume.

• Estilo "Salto Mágico" (Backtracking Não-Cronológico):

  • Como funciona: Se o detetive percebe que está no caminho errado, ele usa um "salto" para voltar muito mais longe no tempo, pulando várias etapas de uma vez. Ele também usa os bilhetes que escreveu (as regras de "não volte aqui") para pular diretamente para áreas promissoras.
  • Vantagem: É muito rápido para encontrar o melhor tesouro rapidamente.
  • Melhor para: Quando você quer apenas o "Top 1" ou o "Top 10" (os melhores). Ele é agressivo em cortar caminhos ruins.

Por que isso é importante?

Antes desse trabalho, se você quisesse as "10 melhores explicações" para um erro em um sistema complexo, teria que usar ferramentas que não foram feitas para isso, o que era lento e ineficiente.

Com o WME, os computadores agora podem:

1. Filtrar em tempo real: Ignorar soluções ruins enquanto ainda estão sendo construídas.
2. Ser flexíveis: Escolher o melhor método (Passo a Passo ou Salto Mágico) dependendo se você quer muitas soluções boas ou apenas a melhor delas.

Resumo em uma frase

O WME é como dar a um explorador de labirintos um GPS que não só mostra o caminho, mas também avisa: "Ei, esse corredor não leva a nenhum tesouro valioso, vamos cortar caminho e ir direto para as áreas ricas!", permitindo encontrar as melhores soluções de forma muito mais inteligente e rápida.

Resumo técnico

Resumo Técnico: WME – Enumeração de Modelos com Pesos baseada em CDCL

1. O Problema: Enumeração de Modelos com Pesos (WME)

O artigo aborda o problema da Enumeração de Modelos com Pesos (Weighted Model Enumeration - WME). Dada uma fórmula booleana na forma normal conjuntiva (CNF) e uma função de peso sobre as atribuições de variáveis, o objetivo não é apenas encontrar uma solução satisfatória ou contar o total de soluções ponderadas, mas sim enumerar um conjunto específico de modelos com base em seus pesos.

As duas variantes principais do problema são:

• Enumeração Top-k: Encontrar os $k$ modelos com os maiores pesos.
• Enumeração por Limiar (Threshold): Encontrar todos os modelos cujo peso seja maior ou igual a um limiar $\theta$.

Limitações das abordagens existentes:

• AllSAT: Enumera todas as soluções satisfatórias sem considerar pesos, tornando a filtragem pós-processamento computacionalmente proibitiva em espaços de solução grandes.
• Weighted Model Counting (WMC): Calcula a soma global dos pesos, mas não fornece acesso aos modelos individuais.
• MaxSAT: Otimiza para encontrar um único modelo de peso máximo, mas carece de mecanismos nativos para ranqueamento incremental ou enumeração baseada em limiar.

O trabalho identifica que não existe suporte nativo em solucionadores (solvers) para essa tarefa, exigindo uma integração profunda de raciocínio ponderado no ciclo de busca do solucionador.

2. Metodologia e Algoritmos

Os autores propõem um framework nativo baseado em CDCL (Conflict-Driven Clause Learning) que estende a lógica booleana tradicional com dimensões numéricas. A abordagem integra propagação de pesos, poda baseada em pesos e análise de conflitos ponderada.

Componentes Chave:

• Propagação e Poda Baseada em Pesos:

  • O solucionador mantém duas quantidades durante a busca: o peso parcial atual ($w(\mu)$) e um limite residual otimista ($I_{max}(\mu)$), que representa o produto dos melhores pesos possíveis para as variáveis ainda não atribuídas.
  • Condição de Poda: Se $w(\mu) \cdot I_{max}(\mu) < \theta$, o ramo é considerado inviável (nenhuma extensão pode atingir o limiar). Isso permite podar grandes partes do espaço de busca antes mesmo de atribuir todas as variáveis.

• Análise de Conflito de Peso (Weight Conflict Analysis):

  • Quando a poda ocorre, o solver gera um cláusula de conflito de peso ($C_w$).
  • Utiliza-se uma estratégia greedy para identificar o conjunto mínimo de literais no caminho atual que, se mantidos, impedem o alcance do limiar. A cláusula aprendida bloqueia a reocorrência desse conjunto específico de atribuições.

• Backtracking Consciente de Resíduo (Residual-Aware Backtracking):

  • Especificamente para enumeração Top-k, quando um novo modelo de alto peso é encontrado e o limiar $\theta$ é atualizado (apertado), o solver não precisa continuar a busca do ponto atual.
  • O algoritmo retrocede (backtracks) diretamente para o nível de decisão mais alto onde o limite otimista ainda excede o novo $\theta$, ignorando ramos que agora são sabidamente inferiores.

• Prioridade de Variáveis:

  • O framework distingue entre variáveis relevantes para o peso e irrelevantes (ex: variáveis auxiliares de codificação Tseitin com pesos simétricos). A heurística de decisão prioriza as variáveis relevantes para acelerar a convergência do peso.

3. Abordagens de Backtracking: Cronológico vs. Não-Cronológico

O artigo explora e compara duas implementações distintas do framework WME:

1. Backtracking Cronológico (WME-CB):

   • Utiliza travessia sequencial. O bloqueio de modelos já explorados é implícito (o solver nunca revisita um ramo fechado).
   • Vantagens: Baixa pegada de memória, propagação rápida.
   • Desvantagens: Sensível à ordem de decisão; não permite reinícios (restarts) sem quebrar a garantia de bloqueio implícito.
   • Melhor cenário: Espaços de solução densos onde a enumeração de muitos modelos é necessária (ex: enumeração por limiar).

2. Backtracking Não-Cronológico (WME-NCB):

   • Utiliza backjumping para o primeiro ponto de implicação única (UIP) e aprendizado de cláusulas explícitas.
   • Vantagens: Robusto à ordem de decisão, permite reinícios, bloqueio explícito de modelos via cláusulas.
   • Desvantagens: Acúmulo de cláusulas de bloqueio aumenta o custo de propagação e o uso de memória.
   • Melhor cenário: Cenários Top-k onde o limiar se ajusta rapidamente, permitindo podas agressivas e direcionamento da busca para soluções de alto peso.

4. Resultados Experimentais

Os autores implementaram as duas variantes (WME-CB e WME-NCB) sobre a base de código CaDiCaL e avaliaram em benchmarks sintéticos e do mundo real (redes bayesianas, instâncias SATLIB).

• Enumeração Top-1 e Top-k:
  • O WME-NCB superou consistentemente o WME-CB e outros solucionadores de estado da arte (como MaxHS e DPO) na tarefa de encontrar o modelo de maior peso.
  • A enumeração nativa Top-k foi significativamente mais eficiente do que a abordagem iterativa de chamar o solver Top-1 repetidamente, pois reutiliza cláusulas aprendidas e limites de peso acumulados.
• Enumeração por Limiar (Threshold):
  • O WME-CB superou o WME-NCB, especialmente em instâncias com muitos modelos satisfatórios. A sobrecarga de gerenciar cláusulas de bloqueio explícitas no WME-NCB prejudicou a propagação em cenários onde a densidade de soluções é alta.
• Estudos de Ablação:
  • Desativar a poda baseada em pesos resultou em degradação severa de desempenho, confirmando que a detecção precoce de conflitos de peso é essencial para a eficiência do algoritmo.

5. Contribuições e Significância

• Definição Formal: Estabelece o WME como uma tarefa de raciocínio de nível de solver, generalizando AllSAT, WMC e MaxSAT.
• Inovação Algorítmica: Introduz mecanismos de aprendizado de cláusulas e análise de conflitos que integram restrições numéricas (pesos) diretamente no loop de CDCL, permitindo poda baseada em limites superiores de peso.
• Exploração Sistemática: Demonstra que não existe uma solução única; a escolha entre backtracking cronológico e não-cronológico depende do regime do problema (densidade de soluções vs. necessidade de otimização rápida).
• Impacto Prático: Oferece uma base para aplicações que exigem explicações probabilísticas, inferência de "top-k" em redes bayesianas e tomada de decisão robusta, onde múltiplas soluções de alta qualidade são necessárias, não apenas a ótima.

Em suma, o trabalho preenche uma lacuna crítica entre a contagem de modelos ponderados e a enumeração de modelos, fornecendo ferramentas nativas para extrair soluções de alta qualidade de forma eficiente em espaços de busca booleanos complexos.