A Resolution-Based Interactive Proof System for UNSAT

1. O Problema

O artigo aborda a assimetria fundamental na verificação de certificados de satisfatibilidade (SAT) e insatisfatibilidade (UNSAT) em lógica proposicional:

• SAT: Se uma fórmula é satisfatível, a prova (uma atribuição de variáveis) pode ser verificada em tempo polinomial.
• UNSAT: Se uma fórmula é insatisfável, as provas atuais (como certificados DRAT ou resoluções) podem ter tamanho exponencial em relação ao tamanho da fórmula. Embora a verificação de um certificado específico seja linear no tamanho do certificado, o tamanho do certificado em si pode ser exponencial (chegando a terabytes em competições recentes).
• Cenário de Aplicação: Isso limita serviços de SAT onde um cliente com recursos computacionais limitados envia uma fórmula para um servidor potente e recebe um certificado para verificação. Se o certificado for exponencialmente grande, o cliente não consegue verificá-lo em tempo viável.

A solução teórica para este problema reside no teorema IP = PSPACE, que garante a existência de protocolos de prova interativos onde o verificador executa em tempo polinomial, independentemente do tamanho da prova. No entanto, protocolos interativos anteriores eram ineficientes para o "Provedor" (exigiam a construção de tabelas verdade completas), tornando-os impraticáveis para algoritmos modernos de SAT. O desafio é criar protocolos interativos que sejam competitivos com algoritmos de SAT práticos (onde o tempo do Provedor no protocolo seja apenas um overhead polinomial em relação ao tempo do algoritmo original).

2. Metodologia

Os autores propõem uma estrutura geral para transformar algoritmos de decisão de UNSAT em protocolos de prova interativos competitivos, baseando-se na técnica de aritmetização (fundamental para IP = PSPACE).

• Definição de Competitividade: Um protocolo é competitivo para um algoritmo Alg se o tempo de execução do Provedor no protocolo for limitado por um polinômio multiplicado pelo tempo de execução de Alg.
• Aritmetização Compatível: O núcleo da metodologia é a definição de uma "aritmetização compatível" com um algoritmo.
  • Uma fórmula é mapeada para um polinômio sobre um corpo finito.
  • O valor do polinômio em uma atribuição binária deve determinar a satisfatibilidade da fórmula (0 para satisfazível, não-zero para insatisfatível, ou vice-versa).
  • Condição de Compatibilidade: Para cada passo macro do algoritmo (transformando a fórmula $\phi_i$ em $\phi_{i+1}$), deve existir uma operação polinomial $P_M$ que simule essa transformação e comute com avaliações pariais (substituição de variáveis).
• O Desafio da Resolução: O artigo demonstra que as aritmetizações padrão (como a usada em provas de IP = PSPACE para QBF) não são compatíveis com o procedimento de resolução de Davis-Putnam devido a propriedades de comutatividade falharem.
• Solução Proposta: Os autores introduzem uma aritmetização não padrão (denotada por $B$) que utiliza potências cúbicas ($x^3$) para literais negativos e combinações específicas de soma e produto. Eles provam matematicamente que essa aritmetização específica satisfaz as condições de compatibilidade com os passos de resolução completa ($R_x$) e limpeza completa ($C_x$) do algoritmo de Davis-Putnam.

3. Contribuições Principais

1. Teorema de Redução: Provar que encontrar um protocolo interativo competitivo para um algoritmo de UNSAT reduz-se a encontrar uma aritmetização compatível com esse algoritmo.
2. Primeiro Protocolo para Davis-Putnam: Apresentar o primeiro protocolo de prova interativo competitivo para o procedimento de resolução de Davis-Putnam (uma versão simplificada e clássica do algoritmo de resolução).
3. Aritmetização Não Padrão: Demonstrar que, ao contrário do que se acreditava, aritmetizações não convencionais podem ser necessárias para compatibilizar protocolos interativos com algoritmos de resolução, superando as limitações das aritmetizações padrão.
4. Implementação e Avaliação: Desenvolver uma ferramenta chamada icdp (Interactively Certified Davis-Putnam) que implementa tanto o Provedor quanto o Verificador, permitindo a comparação empírica entre certificação convencional e interativa.

4. Resultados Experimentais

Os autores realizaram experimentos comparando a certificação interativa (icdp) com a certificação convencional (envio de prova de resolução) e com certificadores modernos (DRAT via kissat).

• Tempo do Verificador:
  • A certificação interativa é vários ordens de magnitude mais rápida para o Verificador em comparação com a certificação convencional.
  • Enquanto o verificador convencional (DRAT-trim) leva centenas de milissegundos, o verificador interativo leva frações de milissegundos (até 0.2ms nos testes), confirmando a vantagem teórica de tempo polinomial.
• Complexidade de Comunicação:
  • O tamanho dos dados transmitidos na certificação interativa cresce muito mais lentamente do que o tamanho das provas de resolução convencionais.
  • A relação parece seguir uma lei de potência inversa: para provars de resolução muito grandes (ex: petabytes), o protocolo interativo exigiria apenas alguns kilobytes de comunicação.
• Tempo e Memória do Provedor:
  • Tempo: O Provedor na configuração interativa é mais lento que na convencional por um fator quase constante (polinomial), mas ainda competitivo em relação ao algoritmo base.
  • Memória: O Provedor interativo consome mais memória (overhead quadrático) porque precisa armazenar as fórmulas intermediárias na ordem inversa para o protocolo, enquanto o algoritmo original processa sequencialmente.
• Comparação com Solvers Modernos:
  • Ao comparar com o solver moderno kissat (que usa CDCL), o icdp (baseado em Davis-Putnam) é significativamente mais lento no tempo de resolução (5 ordens de magnitude), devido à ineficiência intrínseca do algoritmo de Davis-Putnam em comparação com CDCL. No entanto, a vantagem do Verificador interativo permanece.

5. Significado e Conclusão

O trabalho é um marco teórico e prático por demonstrar que certificação interativa competitiva é possível para algoritmos de resolução, não apenas para algoritmos de força bruta.

• Implicações Teóricas: Valida a ideia de que a complexidade do Verificador pode ser reduzida de exponencial para polinomial sem sacrificar drasticamente a eficiência do Provedor, desde que se utilize a aritmetização correta.
• Limitações e Futuro: O protocolo atual é limitado ao algoritmo de Davis-Putnam, que é obsoleto em comparação com solvers modernos baseados em CDCL. O grande desafio aberto é estender essa técnica de aritmetização compatível para algoritmos modernos de SAT (como CDCL) ou QBF baseados em BDDs.
• Aplicabilidade: Embora o algoritmo base não seja o estado da arte, o trabalho prova o conceito de que serviços de SAT distribuídos podem oferecer verificações de insatisfatibilidade extremamente leves para clientes, desde que o servidor utilize algoritmos compatíveis com a aritmetização proposta.

Em resumo, o artigo abre um novo caminho para a verificação de provas de insatisfatibilidade em ambientes com restrições de recursos no lado do verificador, superando a barreira do tamanho exponencial das provas tradicionais através de interatividade e álgebra polinomial.