Automated Reencoding Meets Graph Theory

Resumen Técnico: Automating Reencoding Meets Graph Theory

1. Planteamiento del Problema

Los solucionadores de satisfacibilidad booleana (SAT) modernos han demostrado un rendimiento excepcional en la práctica, pero su comportamiento teórico sigue siendo un desafío. Una de las técnicas de preprocesamiento más influyentes es la Adición de Variables Acotadas (Bounded Variable Addition - BVA). BVA introduce variables auxiliares para recodificar fórmulas de entrada en fórmulas equisatisfiables con menos cláusulas, mejorando así la eficiencia de los solucionadores.

A pesar de su utilidad empírica (BVA y sus variantes como SBVA han sido clave en ganadores de competiciones SAT recientes), existe un vacío teórico significativo:

• No se comprende bien qué tipos de fórmulas pueden ser recodificadas por BVA.
• No se conocen los límites teóricos de la compresión que BVA puede lograr.
• Se desconoce si BVA puede generar ciertas codificaciones óptimas conocidas (como la codificación de producto para la restricción "a lo más uno").
• Las implementaciones actuales (como factor en CaDiCaL/Kissat) tienen una complejidad temporal alta ($\Omega(n^3)$), lo que limita su escalabilidad.

El objetivo del artículo es proporcionar una caracterización teórica rigurosa de BVA, específicamente en el fragmento de fórmulas 2-CNF (cláusulas de dos literales), y utilizar esta comprensión para mejorar su implementación.

2. Metodología: Caracterización mediante Teoría de Grafos

Los autores desarrollan un marco teórico que conecta la lógica proposicional con la teoría de grafos, utilizando el concepto de Redes Rectificadoras Polarizadas Estrictas (Strict Polarized Rectifier Networks - SPRN).

• Representación Gráfica: Transforman fórmulas 2-CNF simples en diagramas (grafos con aristas dirigidas y no dirigidas).
• Correspondencia: Establecen que un paso de BVA corresponde a una operación de reducción de bicliques (subgrafos bipartitos completos) en el grafo asociado.
• Teorema de Caracterización (Teorema 5): Demuestran que una fórmula 2-CNF puede ser obtenida a partir de otra mediante BVA idealizado si y solo si existe una SPRN que "realiza" el diagrama de la fórmula original. Esta caracterización es fundamental porque traduce el problema de recodificación en un problema de construcción de redes de grafos.
• Simplificación Previa: Analizan el impacto de técnicas de pre-preprocesamiento (como la sustitución de literales equivalentes) antes de aplicar BVA, mostrando que esto mejora los límites teóricos.

3. Contribuciones Clave y Resultados Principales

A. Límites Teóricos de Compresión (2-CNF General)
Los autores derivan límites superiores e inferiores para el número de cláusulas en la mejor reencodificación posible mediante BVA para una fórmula 2-CNF con $n$ variables:

• Sin simplificación previa: BVA idealizado puede reducir cualquier fórmula 2-CNF a un máximo de $(1 + o(1)) \frac{n^2}{\lg n}$ cláusulas. Este límite es agudo.
• Con simplificación previa: Si se aplica una rutina de simplificación (sustitución de literales equivalentes), el límite superior mejora a $\left(\frac{\lg 3}{4} + o(1)\right) \frac{n^2}{\lg n} \approx 0.396 \frac{n^2}{\lg n}$.
• Optimalidad: Demuestran que ningún método de reencodificación que produzca 2-CNF puede superar el límite inferior de $\left(\frac{1}{4} - o(1)\right) \frac{n^2}{\lg n}$. Por lo tanto, BVA con simplificación es óptimo hasta un factor constante.

B. Fórmulas Monótonas
Para el subconjunto de fórmulas 2-CNF monótonas (donde todas las cláusulas tienen el mismo signo de polaridad), el límite se reduce aún más a $\left(\frac{1}{4} + o(1)\right) \frac{n^2}{\lg n}$. Esto coincide con el límite inferior para cualquier método de reencodificación, sugiriendo que para fórmulas monótonas, BVA es esencialmente óptimo.

C. La Restricción "A lo más uno" (AtMostOne)
Analizan la restricción AtMostOne ($x_1 \lor x_2, x_1 \lor x_3, \dots$), que tiene $\binom{n}{2}$ cláusulas en su codificación directa.

• Resultado Empírico vs. Teórico: Las implementaciones existentes de BVA reducen esta restricción a $3n - 6$ cláusulas.
• Prueba de Imposibilidad: Utilizando su marco de SPRN, prueban que ninguna implementación de BVA (independientemente de las heurísticas) puede lograr menos de $3n - 6$ cláusulas.
• Implicación: Esto demuestra que la codificación de producto (que usa $2n + o(n)$ cláusulas y es teóricamente más eficiente) no puede ser construida por BVA. BVA tiene una limitación estructural inherente que le impide alcanzar la optimalidad en este caso específico.

D. Implementación Eficiente (BiVA)
Aprovechando trabajos recientes en teoría de grafos sobre particiones de bicliques (Krapivin et al.), los autores desarrollan un nuevo algoritmo llamado BiVA (Biclique Variable Addition).

• Complejidad: Reduce la complejidad temporal de la reencodificación de $\Omega(n^3)$ (en factor) a $O(n^2)$.
• Rendimiento: En fórmulas 2-CNF monótonas aleatorias, BiVA logra una reducción de cláusulas comparable a los métodos existentes pero con una velocidad de ejecución órdenes de magnitud superior.

4. Resultados Experimentales

Los autores evaluaron BiVA frente a factor (Kissat) y la implementación original de BVA en instancias de problemas de conjuntos independientes en grafos aleatorios $G(n, 1/2)$.

• Compresión: La reducción de cláusulas es comparable entre todos los métodos, aunque BiVA individualmente es ligeramente inferior (5-15%). Sin embargo, al combinar BiVA con BVA o factor (ejecutando BiVA primero y luego el otro), se logra una compresión total excelente.
• Tiempo: Las combinaciones (BiVA + BVA/factor) son significativamente más rápidas que ejecutar BVA o factor solos, debido a que el segundo paso se ejecuta sobre una fórmula ya comprimida.
• Variables Auxiliares: BiVA introduce menos variables auxiliares que los métodos puros, aunque las combinaciones tienden a generar más variables en total.

5. Significado e Impacto

Este trabajo es fundamental por varias razones:

1. Fundamentación Teórica: Proporciona la primera caracterización completa de las capacidades y limitaciones de BVA, respondiendo a preguntas abiertas sobre qué estructuras puede o no puede generar.
2. Límites de Optimalidad: Establece que BVA es óptimo para el caso general de 2-CNF (hasta un factor constante), pero identifica casos específicos (como AtMostOne) donde falla en alcanzar la solución óptima conocida, guiando el desarrollo de futuros algoritmos.
3. Avance Práctico: La implementación $O(n^2)$ (BiVA) hace viable el uso de reencodificación avanzada en problemas de gran escala donde las implementaciones anteriores eran prohibitivamente lentas.
4. Conexión Interdisciplinaria: Demuestra cómo herramientas de la teoría de grafos (redes rectificadoras, particiones de bicliques) pueden resolver problemas centrales en la complejidad computacional y la satisfacción booleana.

En conclusión, el artículo no solo explica por qué BVA funciona tan bien en la práctica, sino que define sus fronteras teóricas y ofrece una herramienta más eficiente para explotarlo, cerrando la brecha entre la teoría de la complejidad y la ingeniería de solucionadores SAT.