Resumo Técnico: Aprendizado de Cláusulas de Resolução Estendida via Pontos de Dupla Implicação

Declaração do Problema

Os solucionadores SAT CDCL (Conflict-Driven Clause-Learning) tornaram-se onipresentes na engenharia de software, segurança e inteligência artificial. No entanto, apesar de seu sucesso prático, eles são fundamentalmente limitados por sua dependência do sistema de prova de resolução geral (Res), que é conhecido por ser fraco para certas classes de fórmulas (por exemplo, Princípio da Gavieira, fórmulas de Tseitin). Embora existam sistemas de prova mais fortes, como a Resolução Estendida (ER), e possam fornecer provas de tamanho polinomial para esses casos difíceis, integrar a ER em solucionadores CDCL permanece um desafio significativo. Métodos existentes, como o GlucosER, introduzem variáveis estendidas dinamicamente, mas dependem de padrões específicos de lemas aprendidos (lemas consecutivos compartilhando um sufixo comum) para identificar novas variáveis. Os autores identificam a necessidade de uma abordagem mais flexível e geral para introduzir dinamicamente variáveis estendidas dentro do loop de análise de conflitos do CDCL, a fim de melhorar o desempenho do solucionador em problemas combinatórios difíceis.

Metodologia

O artigo propõe um algoritmo inovador para Aprendizado de Cláusulas de Resolução Estendida (ERCL) implementado dentro do solucionador CDCL MapleLCM, resultando em um novo sistema denominado xMapleLCM. A inovação central é o uso de Pontos de Dupla Implicação (DIPs) para introduzir dinamicamente novas variáveis.

1. Pontos de Dupla Implicação (DIPs)

Um DIP é definido como uma generalização do Ponto de Implicação Único (UIP). Enquanto um UIP é um único literal que domina todos os caminhos do nível de decisão mais alto até o nó de conflito no gráfico de implicação, um DIP é um par de literais $\{x, y\}$ tal que:

• Todo caminho da variável de decisão no nível de decisão mais alto até o nó de conflito passa por pelo menos um nó do par.
• Nem $x$ nem $y$ são um UIP.

Os autores reformularam o problema de encontrar DIPs como encontrar Dois Dominadores de Vértice (TVDs) em um grafo direcionado. Eles utilizam um algoritmo de tempo linear (detalhado em um artigo complementar [BGO24]) baseado no teorema de Menger e na identificação de caminhos disjuntos em vértices para encontrar todos os pares DIP válidos de forma eficiente.

2. Algoritmo ERCL e Introdução de Variáveis

Quando um DIP $\{a, b\}$ é identificado durante a análise de conflitos, o solucionador introduz uma nova variável de extensão $z$ definida como $z \leftrightarrow a \land b$. Isso permite que o solucionador aprenda dois novos tipos de cláusulas:

• Cláusula Pré-DIP: Derivada da implicação de que o primeiro UIP e certos literais de níveis de decisão anteriores implicam o par DIP. Formalmente: $\neg f \lor \neg C \lor z$ (onde $f$ é o primeiro UIP e $C$ representa literais que levam ao DIP).
• Cláusula Pós-DIP: Derivada da implicação de que o par DIP e certos literais levam a um conflito. Formalmente: $\neg z \lor \neg D$.

Este processo efetivamente encurta as cláusulas aprendidas ao substituir conjunções complexas por uma única variável, potencialmente reduzindo o espaço de busca.

3. Implementação e Heurísticas

Os autores implementaram o xMapleLCM como um framework altamente extensível. Decisões heurísticas chave incluem:

• Seleção de DIP: Estratégias incluem escolher o DIP mais próximo do conflito, o DIP "meio" (equilibrando o grafo) ou seleção aleatória.
• Filtragem: Mecanismos para descartar DIPs de baixa qualidade, como exigir uma contagem mínima de ocorrências (por exemplo, 20 ou 50 vezes) ou verificar se a cláusula pós-DIP resultante é uma cláusula "cola" (LBD = 2).
• Aprendizado de Cláusulas: Opções para aprender tanto cláusulas pré quanto pós-DIP ou apenas a cláusula pós-DIP.
• Gerenciamento de Variáveis: Uma estratégia para deletar variáveis estendidas que não estão mais ativas (por exemplo, deletar as 50% piores variáveis a cada 1000 conflitos) para evitar lentidão no solucionador.
• Comutação Adaptativa: Uma heurística que monitora a porcentagem de decisões tomadas em variáveis estendidas. Se essa porcentagem cair abaixo de um limite (3%), o solucionador reverte para o aprendizado padrão 1-UIP para evitar sobrecarga em instâncias onde a ER não é benéfica.

Contribuições Principais

1. Conceito de DIPs: A introdução de Pontos de Dupla Implicação como uma generalização de UIPs, fornecendo uma nova ferramenta estrutural para analisar gráficos de conflito.
2. Algoritmo de Tempo Linear: Um algoritmo eficiente para calcular todos os DIPs no gráfico de implicação, tornando a abordagem viável para uso em tempo de execução em solucionadores SAT.
3. Framework ERCL Flexível: O desenvolvimento do xMapleLCM, um sistema parametrizável que permite aos desenvolvedores experimentar várias políticas de seleção de DIP, filtragem e aprendizado de cláusulas.
4. Validação Empírica: Avaliação extensa demonstrando que o ERCL baseado em DIP supera significativamente o CDCL padrão e outros solucionadores em benchmarks combinatórios difíceis específicos.

Resultados Experimentais

Os autores avaliaram o xMapleLCM contra solucionadores líderes (Kissat, CryptoMiniSat, SBVA-CaDiCaL, GlucosER) em quatro famílias distintas de benchmarks:

• Fórmulas de Tseitin: Em fórmulas de Tseitin baseadas em grade, o xMapleLCM foi o único solucionador a resolver todas as instâncias dentro do limite de tempo de 600 segundos. Embora o GlucosER tenha se saído bem em fórmulas de Tseitin regulares, ele lutou com instâncias baseadas em grade. Solucionadores CDCL padrão (Kissat, SBVA-CaDiCaL) tiveram desempenho pobre.
• Fórmulas Aleatórias k-XOR Xorificadas: O xMapleLCM e o GlucosER superaram significativamente outros solucionadores. O CryptoMiniSat, que usa eliminação gaussiana, teve sucesso apenas em instâncias menores ou configurações específicas de xorificação, falhando em escalar em fórmulas maiores e mais difíceis.
• Problemas de Correspondência de Intervalos: Para essas instâncias insatisfatíveis, nenhum solucionador sem raciocínio de resolução estendida conseguiu resolver qualquer benchmark dentro de um limite de 2 horas. O xMapleLCM e o GlucosER resolveram todas as instâncias, com o xMapleLCM sendo ligeiramente mais lento, mas comparável.
• Competição SAT 2023 Track Principal: Em benchmarks gerais, o xMapleLCM teve desempenho semelhante ao seu solucionador base (MapleLCM). O mecanismo de comutação adaptativa impediu com sucesso a degradação de desempenho em instâncias onde a ER não foi útil, mantendo ao mesmo tempo a capacidade de resolver instâncias específicas difíceis de ER.

Os autores observam que aproximadamente 63% dos conflitos em seus experimentos continham pelo menos um DIP, justificando a necessidade de mecanismos de filtragem. Eles também observaram que o xMapleLCM e o GlucosER identificam conjuntos diferentes de variáveis estendidas (apenas ~25% de sobreposição), sugerindo que capturam propriedades semânticas diferentes.

Significado e Afirmações

O artigo afirma que a resolução estendida pode ser integrada com sucesso em solucionadores CDCL para resolver classes de fórmulas que são de outra forma intratáveis para solucionadores baseados em resolução padrão.

• Complementaridade: O trabalho demonstra que existem múltiplas maneiras válidas de automatizar a ER (abordagem baseada em DIP vs. abordagem baseada em lemas do GlucosER), e ambas podem ser eficazes nas mesmas classes de problemas difíceis.
• Praticidade: Os autores mostram que a sobrecarga de detectar DIPs é negligenciável (tipicamente <2,5% do tempo de execução) e que o método não degrada o desempenho em benchmarks gerais quando heurísticas adaptativas são usadas.
• Direção Futura: O artigo posiciona os DIPs como uma base para pesquisas futuras, incluindo a exploração de Pontos de k-Implicação ($k > 2$) e a aplicação de heurísticas de aprendizado de máquina para ajustar melhor as estratégias ERCL.

Os autores concluem modestamente que, embora tenham identificado famílias específicas onde o ERCL é superior, a questão teórica de saber se o ER baseado em DIP simula totalmente a ER irrestrita permanece aberta e é um alvo para investigação teórica futura.