Finding Connections via Satisfiability Solving

Este artigo apresenta o novo solver upCoP, que combina estratégias de saturação e redução de objetivos em cálculos de conexão de lógica de primeira ordem através de codificações SAT com quebra de simetria para avançar a automação de provas.

O essencial

Imagine que você precisa resolver um quebra-cabeça gigante e complexo, como um labirinto de milhões de caminhos, onde o objetivo é encontrar uma saída (uma prova matemática) que conecte todas as peças corretamente.

Este artigo descreve uma nova maneira de fazer computadores resolverem esses quebra-cabeças lógicos, chamados de "lógica de primeira ordem". Em vez de usar as ferramentas tradicionais que os computadores usam há décadas, os autores criaram um método que transforma o problema inteiro em um jogo de "Verdadeiro ou Falso" (como um Sudoku lógico) e deixa um especialista em resolver esses jogos (um Solver SAT) tomar as decisões.

Aqui está a explicação passo a passo, usando analogias do dia a dia:

1. O Problema: O Labirinto Infinito

Antes, os computadores tentavam resolver esses problemas de duas formas principais:

• Forma 1 (Expansão): Eles criavam novas regras a partir das existentes, como se estivessem plantando árvores infinitas de possibilidades. Isso gasta muita memória e pode criar "galhos mortos" (caminhos que não levam a lugar nenhum).
• Forma 2 (Subdivisão): Eles pegavam o problema grande e tentavam dividi-lo em pedaços menores, voltando atrás (backtracking) se errassem. O problema aqui é que eles podiam visitar o mesmo "caminho morto" várias vezes, desperdiçando tempo.

2. A Solução: O Detetive Inteligente (SAT Solver)

Os autores propõem uma terceira via: Transformar a busca pela prova em um problema de satisfação booleana (SAT).

Pense no Solver SAT (como o CaDiCaL ou o Z3 mencionados no texto) como um detetive super-rápido e organizado.

• Em vez de o computador tentar adivinhar qual caminho seguir, ele cria uma lista de regras: "Se a peça A estiver aqui, a peça B tem que estar ali".
• O detetive usa essas regras para eliminar instantaneamente milhões de combinações impossíveis.
• Se o detetive não consegue encontrar uma solução, ele não apenas diz "não dá", mas entrega um relatório de erro (Unsat Core) explicando exatamente quais regras se contradizem. Isso é como se o detetive dissesse: "Não conseguimos resolver porque a peça X e a peça Y não podem estar juntas".

3. As Três Estratégias (Os "Mapas")

Os autores testaram três maneiras diferentes de desenhar esse "mapa" para o detetive:

• Mapa da Árvore (Tableau): É como tentar desenhar a árvore genealógica completa de uma família. O problema é que a árvore cresce muito rápido e fica confusa. O computador gasta muito tempo apenas desenhando ramos que não vão servir.
• Mapa da Grade (Matriz): Aqui, eles mudaram a estratégia. Em vez de desenhar uma árvore, eles organizam as peças em uma grade (como um tabuleiro de xadrez ou um Sudoku). O objetivo é garantir que todas as peças na grade estejam conectadas a pelo menos uma outra peça. Isso é muito mais eficiente para o "detetive" porque ele vê o quadro todo de uma vez, em vez de focar em um único caminho.
• O Ajuste Fino (Iterative Deepening via Unsat Cores): Às vezes, o detetive precisa de mais peças para resolver o quebra-cabeça. Se ele falha, ele olha o relatório de erro e diz: "Ah, preciso de mais uma cópia da peça 'A'". Ele então pede mais cópias e tenta de novo. Isso evita que ele tente usar peças que nunca serão necessárias.

4. O Grande Truque: Simetria e Economia

Um dos maiores problemas em quebra-cabeças lógicos é a simetria. Imagine que você tem 100 cópias idênticas de uma peça vermelha. O computador pode gastar horas tentando colocar a "cópia 1" no lugar, depois a "cópia 2", depois a "cópia 3", mesmo que todas sejam iguais.

O artigo explica que eles ensinaram o sistema a ignorar essas redundâncias. É como se dissessem ao detetive: "Não tente a peça vermelha número 5 se você já tentou a número 1 e falhou. Elas são a mesma coisa." Isso economiza um tempo enorme.

5. O Resultado: O "UPCoP"

Os autores criaram um novo programa chamado UPCoP para testar essa ideia.

• Eles o colocaram contra o melhor programa do mundo atual (chamado meanCoP).
• O resultado: O UPCoP não venceu em tudo (o antigo ainda é muito forte), mas conseguiu resolver 179 problemas que o antigo não conseguiu.
• Por que? Porque o UPCoP consegue ver o problema de forma diferente, encontrando atalhos (provas menores) que os outros métodos ignoram, e consegue descartar peças inúteis muito mais rápido.

Resumo em uma frase

Os autores criaram um método que transforma a busca por provas matemáticas complexas em um jogo de lógica booleana, permitindo que um "detetive" de computadores elimine milhões de caminhos errados de uma vez só, encontrando soluções que os métodos tradicionais perdem.

É como trocar de tentar escalar uma montanha passo a passo (e cair em buracos) para usar um mapa de satélite que mostra exatamente onde não há caminho, permitindo chegar ao topo de forma muito mais inteligente.

Resumo técnico

Resumo Técnico: Encontrando Conexões via Resolução de Satisfatibilidade

1. O Problema

Os provadores de teoremas automatizados para lógica de primeira ordem (LPO) tradicionalmente utilizam duas estratégias principais de busca:

1. Baseada em Ordenação (Saturação): Provadores como Vampire, E e Spass deduzem novos fatos a partir de um conjunto existente, expandindo o espaço de busca.
2. Redução de Submetas (Backtracking): Sistemas como Setheo e leanCoP manipulam uma prova parcial e realizam backtracking quando necessário.

A classe de redução de submetas sofre com a exploração redundante de fórmulas "úteis" e casos duplicados no espaço de busca, a menos que mecanismos complexos de memória sejam implementados. Além disso, refinamentos globais (como evitar caminhos que levam a becos sem saída) frequentemente envolvem estruturas proposicionais não triviais que são difíceis de gerenciar em provadores tradicionais. O objetivo deste trabalho é superar essas limitações integrando a resolução de Satisfatibilidade (SAT) e Satisfatibilidade Modulo Teorias (SMT) diretamente na busca por provas no Cálculo de Conexão de Bibel.

2. Metodologia

Os autores propõem codificar a própria estrutura da busca por provas de conexão como um problema de satisfatibilidade booleana, em vez de apenas reduzir a lógica de primeira ordem para proposicional via instanciação (como feito em métodos ground). A abordagem central envolve três codificações distintas:

• Codificação de Tableaux de Conexão ($E_T$):

  • Codifica a construção explícita de um tableau fechado.
  • Utiliza variáveis SAT para representar literais em caminhos específicos e operações de extensão/redução.
  • Limitação: Gera um número explosivo de variáveis e perde a estrutura proposicional que os solvers SAT poderiam explorar, degradando-se para uma enumeração exaustiva similar a métodos tradicionais, mas com a sobrecarga de um solver SAT.

• Codificação de Provas em Matriz ($E_M$):

  • Abandona a estrutura de árvore estrita dos tableaux em favor de uma representação matricial.
  • Define uma prova como uma matriz de cláusulas onde cada literal está conectado a pelo menos outro literal de uma cláusula diferente (matriz totalmente conectada) e não existem caminhos abertos.
  • Vantagem: Permite que uma única prova em matriz corresponda a múltiplos tableaux, criando um problema combinatório mais adequado para solvers SAT.
  • Utiliza "seletores" ($S_C$) para escolher quais cópias de cláusulas compõem a matriz.

• Refinamento Iterativo via Núcleos Insatisfatíveis ($E_U$):

  • Resolve o problema de introduzir excessivamente muitas cópias de cláusulas na codificação $E_M$.
  • Utiliza uma abordagem de abstração-refinamento. Inicialmente, assume-se uma multiplicidade baixa de cópias para cada cláusula.
  • Se o solver SAT falha (insatisfatibilidade), extrai-se o núcleo insatisfatível (unsat core). Se o núcleo indicar que mais cópias de uma cláusula específica são necessárias, a multiplicidade dessa cláusula é incrementada e a busca é reiniciada.
  • Isso evita a poluição do espaço de busca com instâncias desnecessárias.

Otimizações e Simetrias:
O artigo propõe técnicas para eliminar redundâncias e simetrias que confundem os solvers SAT:

• Simetria de Multiplicidade: Força a seleção de cópias de cláusulas em ordem (a cópia $i+1$ só é selecionada se a $i$ já estiver selecionada).
• Simetria de Subsumção e Instância: Elimina cláusulas que são subsumidas ou reordena conexões para evitar tentativas equivalentes de prova.
• Simetria de Substituição: Impõe uma ordem nas substituições aplicadas a variáveis em cópias da mesma cláusula para evitar branches simétricos exponenciais.

Implementação:
Os autores implementaram essas técnicas no novo provador UPCoP, que atua como uma camada de propagação de usuário sobre solvers existentes (CaDiCaL para SAT e Z3 para SMT). O UPCoP não gera todas as restrições antecipadamente, mas as adiciona dinamicamente (lazy generation) conforme o solver atribui valores às variáveis.

3. Principais Contribuições

1. Codificação Proposicional de Provas LPO: A primeira codificação que representa a existência de provas de cálculo de conexão como um problema de satisfatibilidade booleana, onde o modelo proposicional é a prova (matriz ou tableau).
2. Três Codificações e Análise Teórica: Apresentação e prova de correção (sonoridade, completude e terminação) para as codificações $E_T$, $E_M$ e $E_U$. A complexidade da codificação de matriz é mostrada como estando na classe $\Sigma^P_2$, alinhada com o limite teórico para problemas de variáveis rígidas.
3. Refinamento via Unsat Cores: Um método inovador para guiar a profundidade iterativa (iterative deepening) usando núcleos insatisfatíveis para determinar dinamicamente quantas cópias de cláusulas são necessárias.
4. Eliminação de Redundância: Técnicas específicas para quebrar simetrias em multiplicidade, subsumção e substituição, essenciais para a eficiência de solvers SAT em problemas de LPO.

4. Resultados Experimentais

O UPCoP foi avaliado no conjunto de benchmarks TPTP (6468 problemas prováveis).

• Desempenho Comparativo: Embora o UPCoP resolva menos problemas no total do que o provador de estado da arte meanCoP, ele demonstrou capacidade única.
• Problemas Exclusivos: O UPCoP resolveu 179 problemas que o meanCoP não conseguiu resolver.
• Motivos do Sucesso:
  1. As provas encontradas pelo UPCoP (em formato de matriz) são frequentemente menores e mais eficientes que as provas em formato de tableau geradas pelo meanCoP.
  2. O uso de unsat cores permite deduzir que certas cláusulas são irrelevantes para uma prova específica, ignorando-as e acelerando a busca.
• Limitações: O sistema pode ficar lento em problemas que exigem a eliminação de conexões não abrangentes, e a sobrecarga de processamento de igualdades de termos pode ser alta se não for gerenciada corretamente.

5. Significado e Impacto

Este trabalho representa uma mudança de paradigma na automação de provas em lógica de primeira ordem. Em vez de usar solvers SAT apenas para verificar instâncias ground (como em métodos de instanciação), o artigo demonstra que é possível codificar a lógica de busca estrutural (conexões, unificação, fechamento de ramos) diretamente no solver SAT.

A abordagem permite que o solver SAT gerencie informações globais e refinamentos complexos de forma nativa, algo difícil para provadores baseados em backtracking puro. A criação do UPCoP e a demonstração de que é possível resolver problemas intratáveis por métodos tradicionais abrem caminho para futuros sistemas híbridos que combinam a força de solvers SAT modernos com a expressividade da lógica de primeira ordem, potencialmente superando as limitações de escalabilidade dos provadores atuais.