Resumen Técnico: Comprensión de los Solutores CDCL mediante Estudios de Escalabilidad y Proofdoors

Enunciado del Problema

A pesar de la intratabilidad teórica de SAT (NP-completo), los solutores de Aprendizaje de Cláusulas Impulsado por Conflictos (CDCL) han demostrado una eficiencia notable en fórmulas industriales grandes, particularmente en la Verificación de Modelos Acotada (BMC) basada en SAT. Si bien existe una extensa investigación empírica sobre el rendimiento de los solutores en conjuntos de pruebas y familias aleatorias/artificiales, hay una brecha significativa en estudios sistemáticos de escalabilidad sobre familias de instancias industriales grandes. Específicamente, sigue sin estar claro cómo escala el rendimiento del solutor con el tamaño del problema (por ejemplo, la profundidad de descomposición en BMC) y qué parámetros estructurales pueden explicar el espectro observado de comportamientos (escalado lineal, polinómico o exponencial). Los intentos previos de explicar esto mediante parámetros estructurales como la anchura arbórea, la relación cláusula-variable (CVR) y la estructura comunitaria han fallado en distinguir entre instancias industriales con escalado lineal y aquellas con escalado exponencial.

Metodología

Los autores realizaron un estudio de escalabilidad integral y un análisis estructural utilizando el siguiente enfoque:

1. Recopilación de Conjuntos de Pruebas y Estudio de Escalabilidad:

   • Conjunto de Datos: Una colección de más de 76.600 instancias CNF derivadas de 766 familias de BMC del conjunto de pruebas HWMCC.
   • Generación: Las instancias se generaron a profundidades de descomposición $K = 1, \dots, 100$ utilizando simpleCAR.
   • Configuración del Solutor: Se utilizó un solutor CDCL moderno (CaDiCaL) con el procesamiento interno, el preprocesamiento y la eliminación de cláusulas desactivados para aislar el comportamiento puro de CDCL.
   • Clasificación: Los tiempos de resolución se suavizaron utilizando una envolvente de máximo móvil para eliminar las oscilaciones de paridad. Las familias se clasificaron como lineales, polinómicas, exponenciales o no clasificadas basándose en el mejor ajuste de modelos de regresión lineal, polinómica y exponencial.

2. Análisis de Parámetros Estructurales:

   • El estudio evaluó parámetros propuestos previamente: Relación Cláusula-Variable (CVR), Anchura Arbórea y Estructura Comunitaria (incluyendo Estructura Comunitaria Jerárquica).
   • Análisis de Proofdoor: Los autores investigaron el parámetro "proofdoor" propuesto recientemente. Un proofdoor es una secuencia de interpolantes entre fragmentos de una fórmula, que representa la memorización del esfuerzo de razonamiento del solutor.
   • Cálculo: Se calcularon tres tipos de interpolantes para cada corte en la descomposición de la fórmula: el más fuerte ($I_s$), el más débil ($I_w$) y un interpolante de McMillan ($I_m$).
     • BVESPC: Utilizó eliminación acotada de variables para calcular los proofdoors más fuertes.
     • IPCCP: Utilizó iZ3 para calcular interpolantes de McMillan.
   • Pruebas de Absorción: Los autores probaron si los solutores CDCL "absorben incrementalmente" estos proofdoors. Una cláusula se absorbe si la propagación de unidades deriva sus consecuencias sin aprender explícitamente la cláusula. La absorción incremental implica que el solutor está calculando efectivamente la secuencia de proofdoors paso a paso.

3. Experimentos de Perturbación:

   • Las instancias con escalado lineal se "barajaron" permutando iteraciones o cláusulas para interrumpir el orden natural de las variables. Se midió el impacto en el tamaño del proofdoor y el rendimiento del solutor.

Contribuciones y Resultados Clave

1. Espectro de Comportamientos de Escalabilidad

El estudio reveló un espectro diverso de comportamientos de escalabilidad dentro del mismo conjunto de pruebas, sin una distinción sintáctica obvia entre regímenes:

• Lineal: 333 familias
• Polinómico: 268 familias
• Exponencial: 148 familias
• No clasificado: 17 familias

2. Fallo de los Parámetros Estructurales Tradicionales

Los autores demostraron empíricamente que los parámetros tradicionales fallan en discriminar entre los regímenes lineal y exponencial:

• CVR: Permaneció constante en ambos regímenes.
• Anchura Arbórea: Las fórmulas de BMC generalmente tienen una anchura arbórea pequeña, pero este parámetro predice un escalado lineal para todas las familias de BMC (mediante programación dinámica), fallando al explicar los casos exponenciales observados.
• Estructura Comunitaria: La modularidad fue uniformemente alta tanto en familias lineales como exponenciales, volviéndola ineficaz como discriminador.

3. Éxito del Parámetro Proofdoor

El parámetro proofdoor distinguió con éxito los regímenes:

• Instancias Lineales: Se observó que los solutores CDCL absorben incrementalmente proofdoors pequeños. Los proofdoors más fuertes calculados satisficieron las condiciones de "pequeñez" (tamaño de interpolante acotado $c$, anchura de camino de fragmento acotada $w$ y dependencia acotada $s$) requeridas por el Teorema del Proofdoor Pequeño.
• Instancias Exponenciales: Los proofdoors muestreados (más fuertes, más débiles y de McMillan) escalaron exponencialmente con el tamaño de la fórmula. Además, estos proofdoors generalmente no fueron absorbidos incrementalmente por el solutor, lo que indica una falla en la memorización del razonamiento a nivel local.

4. Impacto del Barajado (Orden de Variables)

El barajado de instancias con escalado lineal interrumpió la capacidad del solutor para encontrar proofdoors pequeños:

• Caída de Rendimiento: El barajado aumentó el tiempo de resolución en un promedio del 12% (permutación de iteraciones) y del 256% (permutación de cláusulas).
• Crecimiento del Proofdoor: El tamaño del interpolante de McMillan ($I_m$) aumentó drásticamente (promedio del 4590% para el barajado de iteraciones, 7400% para el barajado de cláusulas).
• Correlación: Esto establece un vínculo entre órdenes de ramificación pobres (inducidos por el barajado), tamaños de proofdoor más grandes y un rendimiento degradado del solutor.

Significado y Afirmaciones

El artículo afirma que el proofdoor es el primer parámetro estructural que:

1. Admite un teorema de tamaño de prueba polinómico (vinculando proofdoors pequeños a pruebas de resolución polinómicas).
2. Rastrea empíricamente el comportamiento de los solutores CDCL en fórmulas industriales, separando con éxito los regímenes de escalado lineal de los exponenciales.

Los autores argumentan que, mientras que los parámetros tradicionales describen la estructura estática de grafos de las fórmulas, los proofdoors capturan el comportamiento de razonamiento semántico del solutor (análisis local y memorización). Los resultados apoyan la hipótesis de que los solutores CDCL logran eficiencia en instancias de BMC lineales calculando incrementalmente proofdoors pequeños, mientras que fallan en hacerlo en instancias exponenciales.

El artículo mantiene una postura modesta en sus afirmaciones, reconociendo que:

• El etiquetado de los regímenes de escalabilidad es estadístico (basado en ajustes de regresión) en lugar de pruebas formales de complejidad.
• La tubería de cálculo de proofdoors agota el tiempo en muchas instancias exponenciales debido a la naturaleza NP-dura del problema.
• Los resultados teóricos sobre CDCL y proofdoors dependen de modelos idealizados (por ejemplo, ramificación no determinista), mientras que los experimentos utilizan un solutor del mundo real.
• El estudio no cubrió en profundidad las familias polinómicas, centrándose principalmente en los extremos lineal versus exponencial.

El trabajo concluye que comprender y optimizar el descubrimiento de proofdoors pequeños (por ejemplo, mediante heurísticas de ramificación que prioricen variables de interfaz) es una dirección prometedora para mejorar los solutores de BMC.