Verification of a DPLL Transition System in Rocq

Imagine um mundo onde os computadores estão constantemente jogando um jogo de alto nível de "Verdadeiro ou Falso". Neste jogo, o computador recebe um enorme nó emaranhado de afirmações lógicas — como uma receita que diz: "Se você adicionar açúcar, também deve adicionar farinha, mas se adicionar farinha, não pode adicionar sal". O objetivo é encontrar uma maneira de seguir a receita sem quebrar nenhuma regra. Este é o problema da Satisfatibilidade (SAT). É o equivalente digital de tentar encaixar um milhão de peças de quebra-cabeça diferentes em uma caixa onde algumas peças são vermelhas, outras são azuis, e as instruções dizem: "Nenhuma vermelha perto de azul".

Por que nos importamos? Porque isso não é apenas um quebra-cabeça lógico; é o motor por trás de quase tudo o que é complexo na computação. Desde o design de microchips até a prova de que um teorema matemático é verdadeiro, os computadores usam resolvedores (solvers) de SAT para navegar nesses labirintos lógicos massivos. Mas aqui está o detalhe: esses resolvedores são incrivelmente complexos. Se um pequeno erro (bug) se esconder no código, o computador pode dizer com confiança que uma prova é válida quando, na verdade, ela é um absurdo. É por isso que matemáticos e cientistas da computação são obcecados pela verificação formal. Pense nisso como a construção de uma rede de segurança super rigorosa e inquebrável. Em vez de apenas esperar que o computador funcione, eles usam um tipo especial de "microscópio matemático" (chamado de assistente de prova) para verificar cada passo da lógica, garantindo que a máquina nunca minta sobre a resposta.

A Grande Aventura do Artigo: Construindo uma Máquina de Lógica Confiável

Neste artigo, Julia Dijkstra e Benedikt Ahrens dão um grande salto para tornar essas máquinas de lógica confiáveis. Eles não apenas escreveram um programa; eles construíram um esqueleto matematicamente provado de um famoso método de resolução de lógica chamado DPLL (Davis-Putnam-Logemann-Loveland) dentro de uma ferramenta chamada Rocq.

Pense no método DPLL não como um robô rígido seguindo um roteiro, mas como um jogo de "Troca de Estado". Imagine um detetive tentando resolver um mistério. O detetive começa com um caderno vazio (sem pistas). Eles têm um conjunto de regras para como atualizar seu caderno:

1. A Regra do "Ah, entendi!" (Propagação de Unidade): Se uma pista diz "O mordomo fez ou a empregada fez", e o detetive já sabe que a empregada é inocente, o caderno deve ser atualizado para dizer "O mordeto fez". O detetive não tem escolha; a lógica força o movimento.
2. A Regra do "Palpite Puro" (Literal Puro): Se o detetive vê uma pista sobre "O jardineiro", mas nunca vê uma pista sobre "O jardineiro não fazer algo", ele pode assumir com segurança que o jardineiro está envolvido sem medo de contradição.
3. A Regra do "Ramificando" (Decisão): Se o detetive estiver travado, ele escolhe uma pista aleatória (como "O mordomo fez") e a escreve como uma decisão. Isso é uma bifurcação no caminho.
4. A Regra do "Ops, Caminho Errado" (Backtrack/Retrocesso): Se o detetive escreve uma decisão e depois encontra uma contradição (uma pista que diz "O mordomo não fez"), ele tem que apagar tudo o que aconteceu depois daquela decisão, inverter a decisão (agora o mordomo não fez) e tentar novamente.
5. A Regra do "Fim de Jogo" (Falha): Se ele apagar tudo, inverter a última decisão e ainda assim encontrar uma contradição, o jogo acabou. O mistério é insolúvel.

O principal feito dos autores é pegar todo esse jogo e escrevê-lo em uma linguagem que o assistente de prova Rocq possa ler e verificar. Eles não disseram apenas: "Isso parece correto". Eles provaram três coisas massivas:

• Corretude: Se o jogo terminar com uma solução, essa solução é definitivamente real. O computador não vai alucinar um modelo.
• Completude: Se uma solução existe, o jogo irá encontrá-la. O computador não ficará travado ou desistirá quando não deveria.
• Terminação: O jogo nunca rodará para sempre. É matematicamente garantido que ele parará, seja com uma solução ou com um "Fim de Jogo".

Adicionando um Novo Toque: A Regra "Pura"

Uma das contribuições legais do artigo é que eles adicionaram uma regra específica ao seu jogo que algumas versões anteriores desta teoria deixaram de fora: a Regra do Literal Puro. Na analogia do detetive, este é o momento em que o detetive percebe: "Ei, eu nunca vi nenhuma evidência contra o jardineiro, então vou apenas assumir que o jardineiro é o culpado". Os autores provaram que adicionar esta regra torna o jogo mais rápido sem quebrar nenhuma das garantias de segurança. Eles mostraram que, mesmo com este atalho extra, a lógica permanece hermética.

Da Teoria para um Robô Real (Mas Simples)

Depois de provar que as regras do jogo funcionam perfeitamente na teoria, os autores perguntaram: "Podemos realmente construir um robô que jogue este jogo?". Eles criaram uma estratégia — um conjunto de instruções para o detetive sobre qual regra escolher a seguir. Eles construíram uma versão concreta desta estratégia no Rocq e então usaram uma ferramenta mágica chamada extração para transformar sua prova matemática em um programa de computador real escrito em OCaml.

Eles testaram este novo robô em alguns quebra-cabeças simples. Funcionou! Ele resolveu problemas corretamente, incluindo um quebra-cabeça chamado zebra.cnf com 155 variáveis e 1.135 cláusulas. No entanto, os autores são muito honestos sobre as limitações do robô. É como um carro de brinquedo de prova de conceito: ele dirige perfeitamente e prova que o motor funciona, mas não é um carro de Fórmula 1 ainda. É lento porque usa listas simples para lembrar das pistas, enquanto os carros de corrida do mundo real usam memória de alta velocidade. Os autores admitem que esta versão não está pronta para vencer os gigantes industriais usados pelas empresas hoje, mas é um núcleo verificado. É uma fundação pequena e inquebrável sobre a qual futuros solvers mais rápidos e inteligentes podem ser construídos.

O Que Isso Significa para o Futuro

O artigo não afirma ter resolvido o problema de criar o solver de SAT mais rápido do mundo. Em vez disso, afirma ter construído o projeto (blueprint) mais seguro possível. Ao provar as regras abstratas no Rocq, eles criaram um "núcleo confiável". Pesquisadores futuros agora podem pegar este projeto e adicionar as funcionalidades avançadas dos solvers modernos — como "aprender com os erros" (aprendizado de cláusulas) ou "saltar vários passos para trás" (backtracking não cronológico) — com a confiança de que a lógica subjacente ainda é sólida.

Em suma, Dijkstra e Ahrens não construíram apenas um carro melhor; eles construíram o projeto de um carro que nunca pode bater, provando que a lógica por trás das rodas é matematicamente perfeita. É um passo verificado e pequeno que pavimenta o caminho para máquinas de lógica muito maiores, mais complexas e confiáveis no futuro.