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

Resumen Técnico: CDCL Guiado por Bits Probabilísticos para la Resolución de SAT usando Suposiciones de Consenso Ising

1. Enunciado del Problema

Los solucionadores de Satisfacibilidad Booleana (SAT), particularmente aquellos basados en Aprendizaje de Cláusulas Impulsado por Conflictos (CDCL), son fundamentales para la verificación de hardware, el criptoanálisis y los flujos de trabajo de seguridad. Aunque los solucionadores CDCL modernos son robustos, a menudo requieren un esfuerzo de búsqueda sustancial —medido en conflictos y propagaciones— antes de identificar regiones productivas del espacio de búsqueda para instancias satisfacibles. El desafío central abordado en este artículo es cómo reducir este esfuerzo de búsqueda interno sin comprometer las garantías de corrección del solucionador CDCL. Los autores investigan si muestras estocásticas de baja violación provenientes de un muestreador Ising de bits probabilísticos (p-bit) pueden guiar a un solucionador CDCL hacia una asignación satisfacible de manera más eficiente, asegurando al mismo tiempo que el resultado final permanezca verificado por el motor CDCL completo.

2. Metodología

El marco propuesto es una arquitectura híbrida donde un muestreador Ising de p-bit actúa como una guía heurística para un solucionador CDCL estándar (específicamente CaDiCaL vía PySAT). El flujo de trabajo procede de la siguiente manera:

• Mapeo a Energía Ising: La fórmula CNF de entrada se mapea a una función de energía estilo Ising donde las variables binarias se representan como espines ($s_i \in \{-1, +1\}$). La función de energía penaliza las cláusulas violadas. Las penalizaciones de cláusulas de orden superior se manejan mediante cuadratización de Rosenberg, introduciendo espines auxiliares ($z$) para formar un hamiltoniano cuadrático.
• Muestreo Estocástico: Un motor de p-bit muestrea $R$ réplicas independientes del sistema. El proceso de muestreo implica recocer la temperatura inversa $\beta$ desde una configuración alta (exploratoria) a una baja (explotadora).
• Selección de Suposiciones:
  • Las muestras se clasifican por su recuento directo de violaciones CNF $V(s)$, en lugar de la energía Ising cruda, para asegurar la relevancia con la fórmula original.
  • De las $k$ mejores muestras con menor violación, el sistema calcula una puntuación de acuerdo para cada variable. Las variables donde las $k$ mejores muestras asignan el mismo valor se identifican como "literales de alto acuerdo".
  • Estos literales se ponderan adicionalmente mediante una puntuación de magnetización ponderada por calidad, otorgando mayor influencia a las muestras con menos violaciones.
  • Los $H$ mejores candidatos clasificados se convierten en un conjunto de suposiciones temporales ($\rho_{pbit}$).
• Protocolo de Resolución Híbrida:
  • Intento: Se invoca el solucionador CDCL con $\rho_{pbit}$ como suposiciones duras, sujeto a un presupuesto de conflictos $B_1$.
  • Reintento: Si el primer intento falla o agota el presupuesto, se realiza un segundo intento con un presupuesto $B_2$.
  • Respuesta de Emergencia: Si ambos intentos guiados fallan, el solucionador cambia a CDCL sin restricciones y sin suposiciones. Esta respuesta de emergencia asegura que el método permanezca completo (preservando la corrección SAT/UNSAT).
• Puerta de Idoneidad (Exploratoria): El artículo explora un clasificador de aprendizaje automático (Bosque Aleatorio) entrenado para predecir si una instancia de fórmula específica se beneficiaría del enfoque híbrido. Esta puerta utiliza características estructurales y estadísticas de una ejecución de muestreo de p-bit corta y de bajo costo (sonda) para decidir si enrutar la fórmula hacia la ruta híbrida o hacia CDCL puro.

3. Contribuciones Clave

El artículo presenta las siguientes contribuciones específicas:

• Pipeline Híbrido: Una nueva pipeline que integra el muestreo p-bit/Ising con CDCL, donde las muestras estocásticas generan suposiciones temporales en lugar de reemplazar al solucionador.
• Formulación de la Guía: Una formalización del mecanismo de guía utilizando energía de violación de cláusulas, acuerdo de muestras y magnetización para seleccionar suposiciones.
• Evaluación Empírica: Una evaluación exhaustiva en familias SATLIB satisfacibles seleccionadas, incluyendo 3-SAT Aleatorio (RTI), Subinstancias Mínimas de Espalda (BMS) y 3-SAT Aleatorio con Espalda Controlada (CBS).
• Análisis de Sensibilidad de Distribución: Caracterización de la varianza en el rendimiento del método a través de diferentes clases de instancias, identificando que los beneficios no son universales sino sensibles a la distribución.
• Atribución de Mejoras: Diferenciación entre mejoras derivadas de la calidad directa de las suposiciones versus efectos de "ruta de rescate" (donde los intentos guiados fallidos generan cláusulas aprendidas que ayudan a la respuesta de emergencia sin restricciones posterior).
• Puerta Exploratoria: Resultados iniciales sobre una puerta de idoneidad, destacando el potencial para puertas aprendibles mientras se reconocen las limitaciones actuales respecto a la fuga de características.

4. Resultados Experimentales

El marco se evaluó en 4.800 fórmulas CNF a través de cinco familias. Los hallazgos clave incluyen:

• Rendimiento en CBS y RTI: En instancias de 3-SAT Aleatorio con Espalda Controlada (CBS) y 3-SAT Aleatorio (RTI), el método híbrido logró reducciones significativas en el esfuerzo de búsqueda:
  • Conflictos: Reducidos en un 80.8% – 85.5% (mediana).
  • Propagaciones: Reducidas en un 80.2% – 84.6% (mediana).
  • La reducción fue consistente a través de diversas densidades de cláusulas y tamaños de espalda.
• Rendimiento en BMS: Las Subinstancias Mínimas de Espalda mostraron mejoras más moderadas (reducción de conflictos del 37.8%). Los autores notan que una parte significativa de esta ganancia (tasa de rescate del 100%) proviene del efecto de "ruta de rescate" (reutilización de cláusulas) en lugar de la calidad de las propias suposiciones.
• Rendimiento en Coloreado de Grafos: El método tuvo un rendimiento pobre en instancias de coloreado de grafos.
  • Plano: Reducción de conflictos del 22.8%.
  • Mundo Pequeño (sw): El método híbrido en realidad aumentó las propagaciones medianas en un 1.8% y mostró una reducción de conflictos del 0%, a pesar de tener la estadística de acuerdo de muestras más alta ($q_{abs} = 0.638$). Esto indica que una fuerte polarización de muestras no garantiza suposiciones CDCL útiles.
• Resultados de la Puerta: Una puerta de Bosque Aleatorio entrenada sobre los datos logró un 94.8% de recuperación (reteniendo el 94.8% de las victorias híbridas) mientras enrutaba el 87.5% de las fórmulas hacia la ruta híbrida. Sin embargo, los autores enfatizan que estos resultados están "contaminados por fuga" debido a la inclusión de características derivadas de oráculos y están destinados como un límite superior diagnóstico en lugar de un clasificador listo para implementación.

5. Significado y Afirmaciones

El artículo enmarca modestamente su contribución como un estudio de reducción del esfuerzo de búsqueda en lugar de una afirmación de aceleración universal del tiempo de ejecución.

• Preservación de la Corrección: El significado principal es que el método retiene la completitud de CDCL. La etapa de p-bit es puramente heurística; la corrección está garantizada por el mecanismo de respuesta de emergencia de CDCL.
• Sensibilidad de Distribución: Los autores declaran explícitamente que el método es efectivo solo para ciertas clases de instancias (específicamente 3-SAT aleatorio y con espalda controlada) y puede ser perjudicial o neutral en otras (como el coloreado de grafos de mundo pequeño).
• Direcciones Futuras: El artículo concluye que, aunque la guía de p-bit muestra promesa para reducir los contadores internos de CDCL, el trabajo futuro debe abordar la fuga de características en los modelos de puerta, establecer líneas base de atribución para aislar la calidad de las suposiciones de los efectos de rescate, y validar el enfoque en CNFs motivados por seguridad (por ejemplo, aquellos con estructuras XOR o restricciones ruidosas) que difieren estructuralmente de los puntos de referencia aleatorios utilizados aquí.

El trabajo no afirma reemplazar a CDCL ni proporcionar aceleraciones de extremo a extremo en tiempo de reloj (debido a la naturaleza de prototipo en Python del muestreador de p-bit), sino que demuestra que las muestras estocásticas de baja violación pueden podar eficazmente el espacio de búsqueda para distribuciones específicas de problemas.