Resumen Técnico: Aprendizaje de Cláusulas de Resolución Extendida mediante Puntos de Doble Implicación

Enunciado del Problema

Los solucionadores SAT de Aprendizaje de Cláusulas Impulsado por Conflictos (CDCL) se han vuelto ubicuos en la ingeniería de software, la seguridad y la inteligencia artificial. Sin embargo, a pesar de su éxito práctico, están fundamentalmente limitados por su dependencia del sistema de demostración de resolución general (Res), que se sabe que es débil para ciertas clases de fórmulas (por ejemplo, el Principio del Palomar, fórmulas de Tseitin). Aunque existen sistemas de demostración más fuertes como la Resolución Extendida (ER) y pueden proporcionar demostraciones de tamaño polinómico para estos casos difíciles, integrar ER en los solucionadores CDCL sigue siendo un desafío significativo. Los métodos existentes, como GlucosER, introducen variables extendidas dinámicamente pero dependen de patrones específicos de lemas aprendidos (lemas consecutivos que comparten un sufijo común) para identificar nuevas variables. Los autores identifican la necesidad de un enfoque más flexible y general para introducir dinámicamente variables extendidas dentro del bucle de análisis de conflictos del CDCL, a fin de mejorar el rendimiento del solucionador en problemas combinatorios difíciles.

Metodología

El artículo propone un algoritmo novedoso para el Aprendizaje de Cláusulas de Resolución Extendida (ERCL) implementado dentro del solucionador CDCL MapleLCM, dando como resultado un nuevo sistema denominado xMapleLCM. La innovación central es el uso de Puntos de Doble Implicación (DIP) para introducir dinámicamente nuevas variables.

1. Puntos de Doble Implicación (DIP)

Un DIP se define como una generalización del Punto de Implicación Único (UIP). Mientras que un UIP es un único literal que domina todos los caminos desde el nivel de decisión más alto hasta el nodo de conflicto en el gráfico de implicación, un DIP es un par de literales $\{x, y\}$ tal que:

• Cada camino desde la variable de decisión en el nivel de decisión más alto hasta el nodo de conflicto pasa por al menos un nodo del par.
• Ni $x$ ni $y$ son un UIP.

Los autores reformulan el problema de encontrar DIPs como la búsqueda de Dos Dominadores de Vértice (TVD) en un grafo dirigido. Utilizan un algoritmo de tiempo lineal (detallado en un artículo complementario [BGO24]) basado en el teorema de Menger y la identificación de caminos disjuntos en vértices para encontrar todos los pares DIP válidos de manera eficiente.

2. Algoritmo ERCL e Introducción de Variables

Cuando se identifica un DIP $\{a, b\}$ durante el análisis de conflictos, el solucionador introduce una nueva variable de extensión $z$ definida como $z \leftrightarrow a \land b$. Esto permite al solucionador aprender dos nuevos tipos de cláusulas:

• Cláusula Pre-DIP: Derivada de la implicación de que el primer UIP y ciertos literales de niveles de decisión anteriores implican el par DIP. Formalmente: $\neg f \lor \neg C \lor z$ (donde $f$ es el primer UIP y $C$ representa los literales que conducen al DIP).
• Cláusula Post-DIP: Derivada de la implicación de que el par DIP y ciertos literales conducen a un conflicto. Formalmente: $\neg z \lor \neg D$.

Este proceso acorta efectivamente las cláusulas aprendidas al reemplazar conjunciones complejas con una sola variable, reduciendo potencialmente el espacio de búsqueda.

3. Implementación y Heurísticas

Los autores implementaron xMapleLCM como un marco altamente extensible. Las decisiones heurísticas clave incluyen:

• Selección de DIP: Las estrategias incluyen elegir el DIP más cercano al conflicto, el DIP "medio" (equilibrando el grafo) o la selección aleatoria.
• Filtrado: Mecanismos para descartar DIPs de baja calidad, como exigir un recuento mínimo de ocurrencias (por ejemplo, 20 o 50 veces) o verificar si la cláusula post-DIP resultante es una cláusula "pegamento" (LBD = 2).
• Aprendizaje de Cláusulas: Opciones para aprender tanto las cláusulas pre como post-DIP o solo la cláusula post-DIP.
• Gestión de Variables: Una estrategia para eliminar variables extendidas que ya no están activas (por ejemplo, eliminar el 50% peor de las variables cada 1000 conflictos) para evitar la ralentización del solucionador.
• Conmutación Adaptativa: Una heurística que monitorea el porcentaje de decisiones tomadas sobre variables extendidas. Si este porcentaje cae por debajo de un umbral (3%), el solucionador vuelve al aprendizaje estándar de 1-UIP para evitar sobrecargas en instancias donde ER no es beneficioso.

Contribuciones Clave

1. Concepto de DIPs: La introducción de Puntos de Doble Implicación como una generalización de los UIPs, proporcionando una nueva herramienta estructural para analizar gráficos de conflictos.
2. Algoritmo de Tiempo Lineal: Un algoritmo eficiente para calcular todos los DIPs en el gráfico de implicación, haciendo viable el enfoque para su uso en tiempo de ejecución en solucionadores SAT.
3. Marco Flexible ERCL: El desarrollo de xMapleLCM, un sistema parametrizable que permite a los desarrolladores experimentar con diversas políticas de selección de DIP, filtrado y aprendizaje de cláusulas.
4. Validación Empírica: Evaluación extensa que demuestra que el ERCL basado en DIP supera significativamente al CDCL estándar y a otros solucionadores en benchmarks combinatorios difíciles específicos.

Resultados Experimentales

Los autores evaluaron xMapleLCM frente a solucionadores líderes (Kissat, CryptoMiniSat, SBVA-CaDiCaL, GlucosER) en cuatro familias de benchmarks distintos:

• Fórmulas de Tseitin: En fórmulas de Tseitin basadas en cuadrícula, xMapleLCM fue el único solucionador que resolvió todas las instancias dentro del límite de tiempo de 600 segundos. Aunque GlucosER funcionó bien en fórmulas de Tseitin regulares, tuvo dificultades con instancias basadas en cuadrícula. Los solucionadores CDCL estándar (Kissat, SBVA-CaDiCaL) tuvieron un rendimiento deficiente.
• Fórmulas k-XOR Aleatorias Xorificadas: xMapleLCM y GlucosER superaron significativamente a otros solucionadores. CryptoMiniSat, que utiliza eliminación gaussiana, solo tuvo éxito en instancias más pequeñas o configuraciones específicas de xorificación, fallando al escalar en fórmulas más grandes y difíciles.
• Problemas de Emparejamiento de Intervalos: Para estas instancias insatisfacibles, ningún solucionador sin razonamiento de resolución extendida pudo resolver ningún benchmark dentro de un límite de 2 horas. xMapleLCM y GlucosER resolvieron todas las instancias, siendo xMapleLCM ligeramente más lento pero comparable.
• Competición SAT 2023 Pista Principal: En benchmarks generales, xMapleLCM tuvo un rendimiento similar a su solucionador base (MapleLCM). El mecanismo de conmutación adaptativa previno con éxito la degradación del rendimiento en instancias donde ER no era útil, mientras que mantenía la capacidad de resolver instancias específicas difíciles de ER.

Los autores señalan que aproximadamente el 63% de los conflictos en sus experimentos contenían al menos un DIP, justificando la necesidad de mecanismos de filtrado. También observaron que xMapleLCM y GlucosER identifican conjuntos diferentes de variables extendidas (solo ~25% de superposición), lo que sugiere que capturan propiedades semánticas diferentes.

Significado y Afirmaciones

El artículo afirma que la resolución extendida puede integrarse con éxito en solucionadores CDCL para resolver clases de fórmulas que de otro modo serían intratables para solucionadores basados en resolución estándar.

• Complementariedad: El trabajo demuestra que existen múltiples formas válidas de automatizar ER (enfoque basado en DIP frente al enfoque basado en lemas de GlucosER), y ambos pueden ser efectivos en las mismas clases de problemas difíciles.
• Practicidad: Los autores muestran que la sobrecarga de detectar DIPs es insignificante (típicamente <2.5% del tiempo de ejecución) y que el método no degrada el rendimiento en benchmarks generales cuando se utilizan heurísticas adaptativas.
• Dirección Futura: El artículo posiciona a los DIPs como una base para futuras investigaciones, incluida la exploración de Puntos de $k$-Implicación ($k > 2$) y la aplicación de heurísticas de aprendizaje automático para ajustar mejor las estrategias ERCL.

Los autores concluyen modestamente que, aunque han identificado familias específicas donde ERCL es superior, la pregunta teórica de si el ER basado en DIP simula completamente la ER ilimitada sigue abierta y es un objetivo para futuras investigaciones teóricas.