Resumo Técnico: Extensão do CDCL para Disjunções de Equações de Paridade

Declaração do Problema

O Aprendizado de Cláusulas Impulsionado por Conflitos (CDCL) é o método dominante para resolução de SAT, mas é fundamentalmente limitado pelo sistema de prova de Resolução. Problemas que exigem tamanho de prova exponencial na Resolução (como fórmulas de Tseitin ou o princípio das pombas bijetivas) são comprovadamente difíceis para o CDCL. Embora alguns solucionadores incorporem fragmentos de sistemas de prova mais fortes — como solucionadores pseudo-booleanos usando Planos de Corte ou solucionadores CNF-XOR que lidam com equações de paridade —, essas abordagens frequentemente tratam o raciocínio de paridade como um módulo separado ou se restringem a formas normais específicas (por exemplo, CNF-XOR).

A lacuna específica abordada por este trabalho é a falta de um algoritmo no estilo CDCL que lide nativamente com fórmulas XNF (Forma Normal XOR-OR-AND). Fórmulas XNF consistem em conjunções de cláusulas lineares, que são disjunções de equações de paridade (por exemplo, $(x \oplus y) \lor \neg(y \oplus z)$). Embora o sistema de prova Res(⊕) (Resolução generalizada para XNF) seja conhecido por ser exponencialmente mais forte que a Resolução para certos problemas, os solucionadores existentes não integram totalmente o raciocínio Res(⊕) no loop do CDCL, nem fornecem uma prova teórica de que um algoritmo no estilo CDCL pode simular polinomialmente o Res(⊕).

Metodologia

Os autores propõem o CDCL(⊕), uma generalização do algoritmo CDCL projetada para operar diretamente sobre fórmulas XNF. A metodologia baseia-se em três componentes principais:

1. Novas Regras de Inferência para Res(⊕):
   Os autores introduzem uma nova caracterização do sistema de prova Res(⊕) que substitui as regras padrão de resolução e enfraquecimento por adição e mudança de base.

   • Adição: De $C \lor f$ e $D \lor g$, deduz-se $C \lor D \lor (f + g)$.
   • Mudança de Base: De $C$, deduz-se qualquer $D$ tal que $C \equiv D$ (semanticamente equivalente).
     Crucialmente, eles definem uma regra de resolução afim onde as equações são "isoladas" (via mudança de base) para permitir o cancelamento via adição. Isso elimina a necessidade do espaço de busca exponencial associado à regra de enfraquecimento, permitindo uma simulação polinomial.

2. Propagação de Unidade com Álgebra Linear:
   Diferentemente do CDCL clássico, que propaga com base em atribuições de literais, o CDCL(⊕) realiza propagação de unidade usando álgebra linear sobre $\mathbb{F}_2$.

   • O solucionador mantém um conjunto de unidades conhecidas (equações) $U$.
   • A propagação verifica se uma cláusula linear $C$ implica uma nova equação $f$ ou uma contradição ($1$) dado $U$.
   • Isso é implementado reduzindo a "negação linear" de uma cláusula (o subespaço de atribuições que falsificam a cláusula) contra o span de $U$. Se a negação da cláusula estiver contida dentro do span de $U$ mais uma única equação $f$, então $f$ é deduzida.

3. Aprendizado de Cláusulas via Análise de Conflito:
   O artigo adapta a estratégia de aprendizado de cláusulas 1-UIP (Primeiro Ponto de Implicação Único) para o contexto XNF. Como os grafos de implicação não se traduzem diretamente para equações lineares, o algoritmo de aprendizado opera semanticamente:

   • Começa com a cláusula de conflito (a razão para a contradição).
   • Aplica iterativamente a mudança de base para isolar a equação responsável pela decisão mais recente.
   • Aplica a regra de adição para combinar a cláusula isolada com a razão do conflito, efetivamente cancelando a variável de decisão.
   • Esse processo se repete até que uma cláusula assertiva seja encontrada (uma cláusula que força uma propagação no nível de decisão atual).

Contribuições Principais

Contribuições Teóricas

• Conexão Bidirecional: O artigo prova que o CDCL(⊕) não apenas produz provas Res(⊕), mas também simula polinomialmente o sistema de prova Res(⊕), dadas decisões não determinísticas e reinícios. Isso espelha a relação clássica entre CDCL e Resolução.
• Nova Caracterização do Sistema de Prova: Os autores fornecem um novo conjunto de regras de inferência (adição e mudança de base) que são polinomialmente equivalentes ao Res(⊕), mas carecem da regra de enfraquecimento, tornando-as adequadas para implementação algorítmica.
• Equivalência de Res(⊕) de Entrada: O artigo prova que a propagação de unidade no CDCL(⊕) é equivalente a um fragmento do Res(⊕) conhecido como Res(⊕) de entrada, generalizando um resultado conhecido para o CDCL clássico.
• Fator de Simulação Melhorado: A prova de simulação melhora o fator polinomial para a relação clássica CDCL/Resolução (igualando o resultado em [7] com um argumento mais simples) otimizando como as decomposições de cláusulas são absorvidas.

Contribuições Práticas

• Implementação Xorcle: Os autores apresentam o Xorcle, um solucionador prova de conceito para CDCL(⊕).
  • Implementa álgebra linear eficiente sobre $\mathbb{F}_2$ usando empacotamento de bits.
  • Introduz CSIDS (Soma Decrescente Independente do Estado da Cláusula), uma nova heurística para seleção de cláusulas que generaliza VSIDS e CMTF para o contexto XNF.
  • Introduz LRUP(⊕), uma extensão do formato de registro de prova LRUP para suportar expressões de paridade.
• Heurísticas para XNF: O artigo detalha adaptações para estruturas vigiadas (ciclando através de cláusulas em vez de manter listas de vigia complexas devido a dependências lineares), procedimentos de decisão (ramificação em equações aleatórias da negação de uma cláusula) e seleção de fase (preferindo falsificar cláusulas).

Resultados Experimentais

Os autores avaliaram o Xorcle em um conjunto de benchmarks incluindo:

• Ascon-128: Uma família 2-XNF relacionada a criptografia.
• k-XNFs Aleatórios e Restritos: Fórmulas sintéticas com números variados de variáveis e equações.
• Fórmulas de Tseitin: Problemas de paridade codificados em CNF conhecidos por serem difíceis para a Resolução.

Principais Descobertas:

• Desempenho em XNF: O Xorcle superou os solucionadores existentes (Kissat, CryptoMiniSAT e 2-Xornado) em benchmarks nativos XNF. Notavelmente, superou o 2-Xornado (um solucionador dedicado a 2-XNF) em instâncias Ascon-128, apesar de usar raciocínio XNF geral.
• Desempenho em Fórmulas de Tseitin: Em fórmulas de Tseitin codificadas em CNF, o Xorcle demonstrou escalabilidade quase polinomial no tempo de execução, enquanto solucionadores baseados em Resolução são conhecidos por exigir tempo exponencial. Isso foi alcançado sem pré-processamento, confiando apenas no raciocínio central do CDCL(⊕).
• Qualidade da Decisão: O Xorcle exigiu significativamente menos decisões do que os solucionadores concorrentes, sugerindo que os mecanismos de ramificação e dedução baseados em paridade são mais eficazes para essas classes de problemas.

Significado e Alegações

O artigo afirma que o CDCL(⊕) fornece o primeiro quadro teórico rigoroso e implementação prática que integra totalmente o raciocínio de paridade no paradigma CDCL.

• Significado Teórico: Estabelece que as limitações do CDCL não são inerentes à estrutura algorítmica, mas ao sistema de prova subjacente (Resolução). Ao mudar para o Res(⊕), o CDCL pode teoricamente resolver problemas que são exponencialmente difíceis para o CDCL padrão.
• Significado Prático: Os resultados sugerem que a resolução nativa de XNF é viável e potencialmente superior à conversão de XNF para CNF ou CNF-XOR. A capacidade de resolver fórmulas de Tseitin em tempo quase polinomial sem pré-processamento destaca o potencial do raciocínio de paridade para superar barreiras de dificuldade conhecidas na resolução de SAT.
• Direções Futuras: Os autores observam modestamente que o Xorcle é uma prova de conceito. Atualmente, carece de várias otimizações padrão do CDCL (por exemplo, exclusão de cláusulas, reinícios avançados, heurísticas dinâmicas) e ainda não generaliza totalmente conceitos como "1-UIP" ou "minimização de cláusulas" para o contexto semântico XNF. O trabalho abre caminho para pesquisas futuras em heurísticas que visam especificamente fórmulas CNF que exigem implicitamente raciocínio de paridade.