Probabilistic-bit Guided CDCL for SAT Solving using Ising Consensus Assumptions

Resumo Técnico: CDCL Guiado por Bits Probabilísticos para Solucionadores SAT usando Suposições de Consenso Ising

1. Declaração do Problema

Os solucionadores de Satisfatibilidade Booleana (SAT), particularmente aqueles baseados em Aprendizado de Cláusulas Orientado por Conflito (CDCL), são fundamentais para verificação de hardware, criptanálise e fluxos de trabalho de segurança. Embora os solucionadores CDCL modernos sejam robustos, eles frequentemente exigem um esforço de busca substancial — medido em conflitos e propagações — antes de identificar regiões produtivas do espaço de busca para instâncias satisfatíveis. O desafio central abordado neste artigo é como reduzir esse esforço de busca interno sem comprometer as garantias de correção do solucionador CDCL. Os autores investigam se amostras estocásticas de baixa violação de um amostrador Ising de bits probabilísticos (p-bit) podem guiar um solucionador CDCL em direção a uma atribuição satisfatória de forma mais eficiente, garantindo, ao mesmo tempo, que o resultado final permaneça verificado pelo motor completo do CDCL.

2. Metodologia

O framework proposto é uma arquitetura híbrida onde um amostrador Ising de p-bit atua como um guia heurístico para um solucionador CDCL padrão (especificamente o CaDiCaL via PySAT). O fluxo de trabalho procede da seguinte forma:

• Mapeamento para Energia Ising: A fórmula CNF de entrada é mapeada para uma função de energia no estilo Ising, onde variáveis binárias são representadas como spins ($s_i \in \{-1, +1\}$). A função de energia penaliza cláusulas violadas. Penalidades de cláusulas de ordem superior são tratadas via quadratização de Rosenberg, introduzindo spins auxiliares ($z$) para formar um Hamiltoniano quadrático.
• Amostragem Estocástica: Um motor de p-bit amostra $R$ réplicas independentes do sistema. O processo de amostragem envolve o recozimento da temperatura inversa $\beta$ de uma configuração alta (exploratória) para uma baixa (exploratória).
• Seleção de Suposições:
  • As amostras são classificadas pela sua contagem direta de violação CNF $V(s)$, em vez da energia Ising bruta, para garantir relevância à fórmula original.
  • Das $k$ melhores amostras com menor violação, o sistema calcula uma pontuação de concordância para cada variável. Variáveis onde todas as $k$ melhores amostras atribuem o mesmo valor são identificadas como "literals de alta concordância".
  • Esses literals são ponderados adicionalmente por uma pontuação de magnetização ponderada pela qualidade, dando mais influência às amostras com menos violações.
  • Os $H$ melhores candidatos classificados são convertidos em um conjunto de suposições temporárias ($\rho_{pbit}$).
• Protocolo de Solução Híbrida:
  • Tentativa: O solucionador CDCL é invocado com $\rho_{pbit}$ como suposições rígidas, sujeito a um orçamento de conflitos $B_1$.
  • Repetição: Se a primeira tentativa falhar ou esgotar o orçamento, uma segunda tentativa é feita com um orçamento $B_2$.
  • Fallback: Se ambas as tentativas guiadas falharem, o solucionador alterna para CDCL irrestrito sem suposições. Esse fallback garante que o método permaneça completo (preservando a correção SAT/UNSAT).
• Gateamento de Adequação (Exploratório): O artigo explora um classificador de aprendizado de máquina (Random Forest) treinado para prever se uma instância de fórmula específica se beneficiaria da abordagem híbrida. Esse gate usa características estruturais e estatísticas de uma execução curta e de baixo custo de amostragem p-bit (sonda) para decidir se deve rotear a fórmula para o caminho híbrido ou para o CDCL puro.

3. Principais Contribuições

O artigo apresenta as seguintes contribuições específicas:

• Pipeline Híbrido: Um pipeline inovador que integra amostragem p-bit/Ising com CDCL, onde amostras estocásticas geram suposições temporárias em vez de substituir o solucionador.
• Formulação de Orientação: Uma formalização do mecanismo de orientação usando energia de violação de cláusulas, concordância de amostras e magnetização para selecionar suposições.
• Avaliação Empírica: Uma avaliação abrangente em famílias SATLIB satisfatíveis selecionadas, incluindo 3-SAT Aleatório (RTI), Sub-instâncias Mínimas de Backbone (BMS) e 3-SAT Aleatório Controlado por Backbone (CBS).
• Análise de Sensibilidade à Distribuição: Caracterização da variância de desempenho do método através de diferentes classes de instâncias, identificando que os benefícios não são universais, mas sensíveis à distribuição.
• Atribuição de Melhorias: Diferenciação entre melhorias derivadas da qualidade direta das suposições versus efeitos de "caminho de resgate" (onde tentativas guiadas falhas geram cláusulas aprendidas que auxiliam o fallback subsequente irrestrito).
• Gateamento Exploratório: Resultados iniciais sobre um gate de adequação, destacando o potencial para gateamento aprendível, ao mesmo tempo que reconhece as limitações atuais relacionadas ao vazamento de características.

4. Resultados Experimentais

O framework foi avaliado em 4.800 fórmulas CNF distribuídas em cinco famílias. As principais descobertas incluem:

• Desempenho em CBS e RTI: Em instâncias de 3-SAT Aleatório Controlado por Backbone (CBS) e 3-SAT Aleatório (RTI), o método híbrido alcançou reduções significativas no esforço de busca:
  • Conflitos: Reduzidos em 80,8% – 85,5% (mediana).
  • Propagações: Reduzidas em 80,2% – 84,6% (mediana).
  • A redução foi consistente através de diferentes densidades de cláusulas e tamanhos de backbone.
• Desempenho em BMS: As Sub-instâncias Mínimas de Backbone mostraram melhorias mais moderadas (redução de 37,8% em conflitos). Os autores observam que uma parte significativa desse ganho (100% de taxa de resgate) decorre do efeito de "caminho de resgate" (reutilização de cláusulas) e não da qualidade das próprias suposições.
• Desempenho em Coloração de Grafos: O método performou mal em instâncias de coloração de grafos.
  • Flat: Redução de 22,8% em conflitos.
  • Small-World (sw): O método híbrido na verdade aumentou as propagações medianas em 1,8% e mostrou 0% de redução em conflitos, apesar de ter a estatística de concordância de amostras mais alta ($q_{abs} = 0,638$). Isso indica que uma forte polarização de amostras não garante suposições CDCL úteis.
• Resultados de Gateamento: Um gate Random Forest treinado nos dados alcançou 94,8% de recall (retendo 94,8% das vitórias híbridas) enquanto roteava 87,5% das fórmulas para o caminho híbrido. No entanto, os autores enfatizam que esses resultados estão "contaminados por vazamento" devido à inclusão de características derivadas de oráculos e destinam-se a ser um limite superior diagnóstico, em vez de um classificador pronto para implantação.

5. Significado e Alegações

O artigo enquadra modestamente sua contribuição como um estudo de redução de esforço de busca em vez de uma alegação de aceleração universal de tempo de execução.

• Preservação da Correção: O significado primário é que o método retém a completude do CDCL. A etapa de p-bit é puramente heurística; a correção é garantida pelo mecanismo de fallback do CDCL.
• Sensibilidade à Distribuição: Os autores afirmam explicitamente que o método é eficaz apenas para certas classes de instâncias (especificamente 3-SAT aleatório e controlado por backbone) e pode ser prejudicial ou neutro em outras (como coloração de grafos small-world).
• Direções Futuras: O artigo conclui que, embora a orientação por p-bit mostre promessa para reduzir contadores internos do CDCL, trabalhos futuros devem abordar o vazamento de características em modelos de gateamento, estabelecer linhas de base de atribuição para isolar a qualidade das suposições dos efeitos de resgate e validar a abordagem em CNFs motivadas por segurança (por exemplo, aquelas com estruturas XOR ou restrições ruidosas), que diferem estruturalmente dos benchmarks aleatórios usados aqui.

O trabalho não alega substituir o CDCL ou fornecer acelerações de ponta a ponta em tempo de relógio (devido à natureza de protótipo em Python do amostrador de p-bit), mas demonstra que amostras estocásticas de baixa violação podem efetivamente podar o espaço de busca para distribuições específicas de problemas.