Resumo Técnico: Generalização do CDCL com Retrocesso em Grafo

Declaração do Problema

O algoritmo de Aprendizado de Cláusulas Impulsionado por Conflito (CDCL) é a abordagem dominante na resolução de satisfatibilidade proposicional (SAT). Os solucionadores atuais dependem principalmente do Retrocesso Não-Cronológico (NCB) ou, mais recentemente, do Retrocesso Cronológico (CB) para reparo de conflitos.

• NCB realiza retrocessos agressivos até o nível de decisão mais alto em uma cláusula aprendida (tipicamente o segundo mais alto), desatribuindo todas as decisões subsequentes e suas consequências. Embora eficiente, essa abordagem impõe uma ordem estrita de cima para baixo que pode forçar a desatribuição de literais que o usuário deseja manter atribuídos, potencialmente levando a retrocessos desnecessários e reduzindo a localidade da busca.
• CB é menos restritivo, retrocedendo apenas até o nível de decisão mais alto menos um, preservando algumas atribuições. No entanto, ele ainda adere a uma ordem temporal rígida baseada em níveis de decisão.

Ambos os métodos abstraem o grafo de implicação em níveis de decisão, criando uma superaproximação grosseira das dependências. Essa abstração restringe a capacidade do solucionador de realizar reparos granulares, potencialmente desfazendo literais "pesados" (caros ou preferidos) que não são estritamente necessários para resolver um conflito.

Metodologia: Retrocesso em Grafo (GB)

Os autores propõem o Retrocesso em Grafo (GB), um esquema inovador que utiliza o grafo de implicação diretamente para determinar quais literais desatribuir, em vez de depender exclusivamente dos níveis de decisão.

Conceitos Principais

1. Blocos: Em vez de agrupar literais por nível de decisão, o GB os agrupa em blocos. Um bloco $ck_\ell$ é definido como o conjunto de todos os literais no grafo de implicação que dependem de um literal de decisão específico $\ell$. Um literal implicado pode pertencer a múltiplos blocos se depender de múltiplas decisões.
2. Função de Peso Definida pelo Usuário: O GB introduz uma função de peso $\zeta: \mathcal{L} \to \mathbb{R}$ que mapeia literais para números reais. Isso permite que os usuários atribuam pesos mais altos a literais que preferem manter atribuídos (por exemplo, literais "pesados").
3. Estratégia de Seleção de Blocos: Ao detectar uma cláusula de conflito $C$, o GB identifica o conjunto de blocos $\gamma(C)$ envolvidos no conflito. Ele seleciona um conjunto de blocos $\Gamma^*$ para desfazer de modo que:
   • Exatamente um bloco de $\gamma(C)$ seja desfeito (para garantir que a cláusula aprendida se torne unitária).
   • O peso total dos literais desfeitos seja minimizado.
   • Salvaguardas de Terminação: Para evitar loops infinitos (onde o mesmo conflito recorre sem aprender novas cláusulas), a seleção é restrita a "candidatos de retrocesso terminantes". Um candidato é válido se levar ao aprendizado de uma nova cláusula ou envolver o bloco mais recente no conflito.

Ajustes Algorítmicos

• Análise de Conflito: A análise padrão de 1-UIP (Ponto de Implicação Único) é adaptada para operar em blocos. O algoritmo resolve cláusulas até que exatamente um literal pertencente ao bloco selecionado $\Gamma^*$ permaneça, gerando uma cláusula aprendida que implica um literal invertido.
• Retrocesso: Diferentemente do NCB/CB, que desatribui um sufixo contíguo da trilha, o GB desatribui blocos específicos. Isso requer recalcular os níveis de decisão para os literais restantes e gerenciar a estrutura da trilha dinamicamente.
• Literais Vigiados e Invariantes: O esquema padrão de dois literais vigiados depende de uma invariante tipo pilha onde os vigiados são desatribuídos antes de outros literais. O GB quebra essa ordem. Para manter a correção, os autores introduzem entre-blocos ($\eta(\ell)$), um conjunto de blocos que, se desfeitos, exigem que o literal $\ell$ seja repropagado. Isso leva a uma invariante revisada (Invariante 2) garantindo que, se um vigiado for desatribuído, o outro vigiado esteja satisfeito ou será repropagado.

Contribuições Principais

1. Generalização: O GB é provado ser uma generalização tanto do NCB quanto do CB. Ao definir funções de peso específicas, o GB pode simular o comportamento do NCB (retrocedendo até o segundo nível mais alto) e do CB (retrocedendo até o nível mais alto menos um).
2. Controle Granular: A abordagem permite reparo de conflitos "cirúrgico", minimizando o número de literais desatribuídos com base nas preferências do usuário (pesos) em vez de apenas na ordem de decisão.
3. Garantias Teóricas: O artigo fornece provas para a correção, completude e terminação do algoritmo GB.
4. Implementação: Os autores implementaram o GB no solucionador experimental NapSAT, incluindo otimizações como:
   • Bloqueadores: Adaptados para o GB com entre-blocos.
   • Fusão de Blocos: Estratégias tanto Eager (ECM) quanto Lazy (LCM) para lidar com implicações perdidas e evitar retrocessos redundantes.
   • Melhor Seleção de Bloco (BB): Uma heurística para equilibrar o compromisso entre minimizar desatribuições e garantir progresso.

Resultados Empíricos

Os autores avaliaram o GB contra NCB, CB e LSCB (Retrocesso Cronológico Forte Preguiçoso) em 1.000 instâncias satisfatíveis de coloração de grafos com 3 cores.

• Propagações: As variantes do GB consistentemente exigiram menos propagações de literais do que as abordagens padrão. A melhor configuração (GB+ECM) alcançou 47% menos propagações do que o NCB.
• Tempo de Execução: A redução nas propagações traduziu-se em uma melhoria de tempo de execução de aproximadamente 30% para a melhor configuração.
• Compensações: Embora o GB reduza o número de desatribuições, o custo por propagação é maior devido à sobrecarga de manter blocos e entre-blocos. No entanto, o efeito líquido em instâncias difíceis foi positivo.
• Reinício: Os autores observaram que os reinícios padrão penalizam o desempenho do GB, pois conflitam com o objetivo do GB de minimizar desatribuições. O GB performa melhor na resolução em tiro único ou em cenários onde a reordenação de decisões é menos crítica do que preservar atribuições específicas.

Significado e Alegações

O artigo alega que o Retrocesso em Grafo oferece uma abordagem mais flexível e guiada pelo usuário para a resolução de SAT. Ao desafiar a abstração dos níveis de decisão, o GB permite que os solucionadores preservem literais "pesados" que, de outra forma, seriam descartados por esquemas de retrocesso agressivos.

Os autores posicionam o GB não como um substituto para todas as estratégias existentes, mas como um quadro geral que subsume o NCB e o CB, enquanto oferece desempenho superior em benchmarks específicos (como coloração de grafos), onde minimizar o escopo do retrocesso é benéfico. Eles destacam seu potencial de aplicabilidade em quadros baseados em AVATAR e resolução SMT, onde a estrutura rígida de pilha do CDCL tradicional pode ser uma limitação, embora reconheçam que a escalabilidade para um número massivo de decisões e a integração com solucionadores de teoria permanecem um desafio aberto.