Resumo Técnico: Compreendendo Solutores CDCL Através de Estudos de Escalabilidade e Proofdoors

Declaração do Problema

Apesar da intratabilidade teórica do SAT (NP-completo), solutores de Aprendizado de Cláusulas Impulsionado por Conflito (CDCL) demonstraram eficiência notável em fórmulas industriais de grande porte, particularmente na Verificação de Modelo Limitada baseada em SAT (BMC). Embora exista pesquisa empírica extensa sobre o desempenho de solutores em benchmarks e famílias aleatórias/artesanais, há uma lacuna significativa em estudos sistemáticos de escalabilidade sobre famílias de instâncias industriais de grande porte. Especificamente, permanece incerto como o desempenho do solutor escala com o tamanho do problema (por exemplo, profundidade de desdobramento em BMC) e quais parâmetros estruturais podem explicar o espectro observado de comportamentos (escalabilidade linear, polinomial ou exponencial). Tentativas anteriores de explicar isso através de parâmetros estruturais como largura de árvore, razão cláusula-variável (CVR) e estrutura de comunidade falharam em distinguir entre instâncias industriais com escalabilidade linear e exponencial.

Metodologia

Os autores conduziram um estudo de escalabilidade abrangente e uma análise estrutural utilizando a seguinte abordagem:

1. Coleta de Benchmarks e Estudo de Escalabilidade:

   • Conjunto de Dados: Uma coleção de mais de 76.600 instâncias CNF derivadas de 766 famílias de BMC do conjunto de benchmarks HWMCC.
   • Geração: Instâncias foram geradas em profundidades de desdobramento $K = 1, \dots, 100$ usando simpleCAR.
   • Configuração do Solutor: Um solutor CDCL moderno (CaDiCaL) foi utilizado com pós-processamento, pré-processamento e deleção de cláusulas desativados para isolar o comportamento puro do CDCL.
   • Classificação: Os tempos de resolução foram suavizados usando um envelope de máximo móvel para remover oscilações de paridade. As famílias foram classificadas como lineares, polinomiais, exponenciais ou não classificadas com base no melhor ajuste de modelos de regressão linear, polinomial e exponencial.

2. Análise de Parâmetros Estruturais:

   • O estudo avaliou parâmetros previamente propostos: Razão Cláusula-Variável (CVR), Largura de Árvore e Estrutura de Comunidade (incluindo Estrutura de Comunidade Hierárquica).
   • Análise de Proofdoor: Os autores investigaram o parâmetro "proofdoor" recentemente proposto. Um proofdoor é uma sequência de interpolantes entre blocos de uma fórmula, representando a memorização do esforço de raciocínio do solutor.
   • Cálculo: Três tipos de interpolantes foram computados para cada corte na decomposição da fórmula: o mais forte ($I_s$), o mais fraco ($I_w$) e um interpolante de McMillan ($I_m$).
     • BVESPC: Utilizou eliminação limitada de variáveis para calcular proofdoors mais fortes.
     • IPCCP: Utilizou iZ3 para calcular interpolantes de McMillan.
   • Teste de Absorção: Os autores testaram se solutores CDCL "absorvem incrementalmente" esses proofdoors. Uma cláusula é absorvida se a propagação unitária deriva suas consequências sem aprender explicitamente a cláusula. A absorção incremental implica que o solutor está efetivamente computando a sequência de proofdoors passo a passo.

3. Experimentos de Perturbação:

   • Instâncias com escalabilidade linear foram "embaralhadas" permutando iterações ou cláusulas para perturbar a ordenação natural das variáveis. O impacto no tamanho do proofdoor e no desempenho do solutor foi medido.

Principais Contribuições e Resultados

1. Espectro de Comportamentos de Escalabilidade

O estudo revelou um espectro diversificado de comportamentos de escalabilidade dentro do mesmo conjunto de benchmarks, sem distinção sintática óbvia entre os regimes:

• Linear: 333 famílias
• Polinomial: 268 famílias
• Exponencial: 148 famílias
• Não Classificada: 17 famílias

2. Falha dos Parâmetros Estruturais Tradicionais

Os autores demonstraram empiricamente que parâmetros tradicionais falham em discriminar entre regimes lineares e exponenciais:

• CVR: Permaneceu constante em ambos os regimes.
• Largura de Árvore: Fórmulas de BMC geralmente possuem pequena largura de árvore, mas este parâmetro prevê escalabilidade linear para todas as famílias de BMC (via programação dinâmica), falhando em explicar os casos exponenciais observados.
• Estrutura de Comunidade: A modularidade foi uniformemente alta em famílias tanto lineares quanto exponenciais, tornando-a ineficaz como discriminador.

3. Sucesso do Parâmetro Proofdoor

O parâmetro proofdoor distinguiu com sucesso os regimes:

• Instâncias Lineares: Observou-se que solutores CDCL absorvem incrementalmente proofdoors pequenos. Os proofdoors mais fortes computados satisfizeram as condições de "pequenez" (tamanho de interpolante limitado $c$, largura de caminho de bloco limitado $w$ e dependência limitada $s$) exigidas pelo Teorema do Proofdoor Pequeno.
• Instâncias Exponenciais: Proofdoors amostrados (mais fortes, mais fracos e de McMillan) escalaram exponencialmente com o tamanho da fórmula. Além disso, esses proofdoors tipicamente não foram absorvidos incrementalmente pelo solutor, indicando uma falha em memorizar o raciocínio localmente.

4. Impacto do Embaralhamento (Ordenação de Variáveis)

O embaralhamento de instâncias com escalabilidade linear perturbou a capacidade do solutor de encontrar proofdoors pequenos:

• Queda de Desempenho: O embaralhamento aumentou o tempo de resolução em uma média de 12% (permutação de iterações) e 256% (permutação de cláusulas).
• Crescimento do Proofdoor: O tamanho do interpolante de McMillan ($I_m$) aumentou dramaticamente (média de 4590% para embaralhamento de iterações, 7400% para embaralhamento de cláusulas).
• Correlação: Isso estabelece um vínculo entre ordens de ramificação pobres (induzidas pelo embaralhamento), tamanhos maiores de proofdoor e desempenho degradado do solutor.

Significância e Alegações

O artigo alega que o proofdoor é o primeiro parâmetro estrutural que:

1. Admite um teorema de tamanho de prova polinomial (ligando proofdoors pequenos a provas de resolução polinomiais).
2. Rastreia empiricamente o comportamento de solutores CDCL em fórmulas industriais, separando com sucesso regimes de escalabilidade linear de exponencial.

Os autores argumentam que, enquanto parâmetros tradicionais descrevem a estrutura de grafo estática das fórmulas, proofdoors capturam o comportamento de raciocínio semântico do solutor (análise localizada e memorização). Os resultados apoiam a hipótese de que solutores CDCL alcançam eficiência em instâncias de BMC lineares computando incrementalmente proofdoors pequenos, enquanto falham em fazê-lo em instâncias exponenciais.

O artigo permanece modesto em suas alegações, reconhecendo que:

• A rotulagem dos regimes de escalabilidade é estatística (baseada em ajustes de regressão) em vez de provas formais de complexidade.
• O pipeline de computação de proofdoor atinge o tempo limite em muitas instâncias exponenciais devido à natureza NP-difícil do problema.
• Os resultados teóricos referentes a CDCL e proofdoors dependem de modelos idealizados (por exemplo, ramificação não determinística), enquanto os experimentos utilizam um solutor do mundo real.
• O estudo não cobriu famílias polinomiais em profundidade, focando principalmente nos extremos linear versus exponencial.

O trabalho conclui que entender e otimizar a descoberta de proofdoors pequenos (por exemplo, via heurísticas de ramificação que priorizam variáveis de interface) é uma direção promissora para melhorar solutores de BMC.