Resumo Técnico: Descobrindo Provas Curtas, Mais Curtas e as Mais Curtas de Fórmulas UNSAT

Declaração do Problema

Os solvers modernos de SAT são ferramentas poderosas capazes de determinar a satisfatibilidade de fórmulas proposicionais e gerar provas de resolução para instâncias insatisfatíveis (UNSAT). Essas provas são essenciais para a verificação, garantindo que a afirmação "UNSAT" do solver esteja correta. No entanto, embora os solvers modernos como o CaDiCaL produzam empiricamente provas relativamente curtas, não há garantia de que estas sejam as mais curtas possíveis.

O problema de encontrar a prova de resolução mais curta é um problema de otimização onde o conjunto viável é o conjunto de todas as provas válidas para uma determinada fórmula, e o objetivo é minimizar o comprimento da prova (número de cláusulas). Este problema é significativamente mais difícil do que simplesmente encontrar uma prova válida, pois o espaço de busca é exponencialmente grande e altamente simétrico. Trabalhos anteriores, como Peitl e Szeider (2021), tentaram resolver isso via codificações SAT, mas foram limitados a fórmulas muito pequenas (até ~12 cláusulas) devido à explosão do espaço de busca e à quebra de simetria incompleta.

Metodologia

Os autores propõem um novo algoritmo de branch-and-bound projetado para enumerar provas de resolução e encontrar a mais curta. O núcleo de sua metodologia baseia-se em três componentes principais: uma nova representação de prova, uma estratégia de ramificação específica e técnicas avançadas de poda.

1. Representação de Lista de Camadas (Layer List)

Para abordar o problema das simetrias de permutação (onde a reordenação de cláusulas cria provas diferentes, mas equivalentes), os autores introduzem uma representação de lista de camadas $(L_0, L_1, \dots, L_n)$.

• Estrutura: $L_0$ contém os axiomas (cláusulas da fórmula original). Cada camada subsequente $L_j$ contém cláusulas derivadas da resolução de uma cláusula da camada imediatamente anterior ($L_{j-1}$) com uma cláusula de qualquer camada anterior ($L_0 \cup \dots \cup L_{j-1}$).
• Propriedade "Pegar ou Deixar" (Take-it-or-leave-it): Uma restrição crucial exige que, se uma cláusula puder ser derivada em uma camada anterior, ela deve ser colocada lá. Isso evita que uma cláusula apareça em uma camada posterior se ela puder ter sido derivada anteriormente.
• Unicidade: O Teorema 2 prova que, para qualquer conjunto de cláusulas que constituem uma prova, existe exatamente uma representação de lista de camadas canônica. Esta representação quebra todas as simetrias decorrentes de permutações de cláusulas, ao contrário das codificações baseadas em DAG anteriores, que poderiam representar o mesmo conjunto de cláusulas com diferentes ordenações topológicas.

2. Busca Branch-and-Bound

O algoritmo trata a construção de uma lista de camadas como uma busca recursiva sobre subproblemas.

• Definição de Subproblema: Um subproblema $P$ rastreia Previous (cláusulas das camadas $0$a$k-1$), Current (cláusulas na camada $k$), Next (cláusulas candidatas para a camada $k+1$) e Forgotten (cláusulas que poderiam ter sido derivadas anteriormente, mas não foram incluídas).
• Particionamento: Em vez de enumerar todos os subconjuntos de resolventes, o algoritmo ramifica em cláusulas candidatas individuais para a próxima camada. Ele decide se inclui uma cláusula candidata no conjunto Next ou se a move para o conjunto Forgotten, explorando efetivamente o espaço de listas de camadas válidas.

3. Poda e Otimização

A busca é guiada por vários procedimentos de poda para eliminar ramos não otimizados:

• Poda de Fronteira (Frontier Pruning): O algoritmo restringe as derivações a cláusulas de "fronteira" (cláusulas não subsumidas por outras cláusulas conhecidas). O Teorema 3 estabelece que qualquer prova usando cláusulas de não-fronteira pode ser transformada em uma prova usando apenas cláusulas de fronteira sem aumentar o comprimento.
• Poda de Dominância: Uma relação de dominância é definida entre subproblemas. Se um subproblema $P'$ domina $P$ (significando que $P'$ usou menos ou igual número de axiomas, pode derivar um superconjunto de cláusulas, possui um superconjunto de fronteiras e esqueceu um subconjunto de cláusulas), então qualquer prova recuperável de $P$ também pode ser recuperada de $P'$ com comprimento igual ou melhor. Subproblemas dominados são descartados.
• Limite Inferior (Lower Bounding): O algoritmo utiliza o tamanho do Menor Subconjunto Insatisfatível Mínimo (SMUS) para estimar um limite inferior no comprimento restante da prova. Especificamente, ele aproveita o fato de que uma prova para uma fórmula minimamente insatisfatível com $m$ cláusulas requer pelo menos $2m-1$ passos. Este limite é generalizado para fórmulas não mínimas usando cálculos de SMUS (aproximados via o pacote Forqes ou uma rotina de branch-and-bound personalizada).

Principais Contribuições

1. Representação de Lista de Camadas: Uma nova codificação de prova que mapeia unicamente qualquer conjunto de cláusulas de prova para uma única estrutura, quebrando todas as simetrias de permutação e superando a quebra de simetria baseada em DAG de estado da arte.
2. Algoritmo Branch-and-Bound: Um procedimento de busca completo que opera em prefixos de listas de camadas, capaz de encontrar a prova de resolução ótima (mais curta).
3. Mecanismos de Poda: Um conjunto de técnicas de poda, incluindo simplificação baseada em fronteira, relações de dominância em subproblemas e limite inferior baseado em SMUS.
4. Capacidade Anytime: O algoritmo funciona como um otimizador anytime, fornecendo limites superiores válidos (provas mais curtas encontradas até o momento) e limites inferiores durante toda a busca.

Resultados Experimentais

Os autores avaliaram sua abordagem em dois conjuntos de dados: fórmulas sintéticas (ex: Pigeonhole, Parity, Random 3-CNF) e instâncias UNSAT da Competição de SAT 2002.

• Redução do Comprimento da Prova:
  • Em fórmulas sintéticas, a abordagem reduziu os comprimentos das provas em 25% a 50% em comparação com o CaDiCaL.
  • Em instâncias da Competição de SAT 2002, as provas foram encurtadas em 30% a 60%.
  • Em casos específicos (ex: fórmulas de cardinalidade de subconjunto), reduções de pelo menos 40% foram observadas consistentemente.
• Otimalidade e Velocidade:
  • Comparado à abordagem de linha de base de Peitl e Szeider (2021), o método proposto resolveu o dobro de instâncias até a otimalidade.
  • Para instâncias resolvidas por ambos, a abordagem proposta reduziu o tempo para a otimalidade em ordens de magnitude (ex: resolvendo fórmulas de 9 cláusulas em segundos vs. milhares de segundos para a linha de base).
  • O método computou com sucesso números de dureza de resolução ($h_m$) para fórmulas de até 8 cláusulas e parcialmente para 9 cláusulas, superando significativamente a linha de base em tempo de execução.
• Limitações:
  • A abordagem é intensiva em memória. Ocorre erro de falta de memória quando o comprimento da prova do CaDiCaL excede aproximadamente $10^6$ passos, pois o algoritmo deve desempacotar e armazenar grandes provas de resolução para analisá-las.
  • A poda de limite inferior é limitada pelo cálculo do SMUS; para certas fórmulas (como Pigeonhole), o limite não é justo o suficiente para podar a busca de forma eficaz.

Significância

O artigo afirma que sua principal significância reside em demonstrar que as provas geradas por solvers de SAT de estado da arte são frequentemente longe de serem ótimas e que essas provas podem ser sistematicamente encurtadas. Ao introduzir uma representação de quebra de simetria e uma busca branch-and-bound eficiente, os autores fornecem um método para:

1. Verificar a Eficiência do Solver: Estimar a "margem para melhoria" em passos de solver, revelando que solvers padrão podem levar de 50% a 200% mais passos do que o necessário.
2. Otimizar Sistemas de Prova: Oferecer um fluxo de trabalho para minimização de prova que é escalável para fórmulas maiores do que métodos exatos anteriores.
3. Avançar a Complexidade de Prova: Fornecer uma ferramenta prática para calcular números de dureza de resolução e explorar a estrutura de provas mínimas, o que tem implicações para entender a complexidade inerente dos problemas de lógica proposicional.

Os autores concluem que, embora sua abordagem tenha limitações de memória para provas muito grandes, ela representa um passo substancial adiante na descoberta automatizada de provas de resolução ótimas, resolvendo mais instâncias de forma mais rápida do que as abordagens de codificação SAT anteriores.