Resumen Técnico: Enumeración Proyectada Disjunta para SAT y SMT sin Cláusulas de Bloqueo

Enunciado del Problema

El artículo aborda los desafíos computacionales inherentes a la Satisfiabilidad de Todas las Soluciones (AllSAT) y su extensión, la Satisfiabilidad de Todas las Soluciones Modulo Teorías (AllSMT). El objetivo es enumerar todas las asignaciones satisfactorias de una fórmula. Mientras que la resolución SAT tradicional termina al encontrar una única solución, la enumeración requiere explorar todo el espacio de búsqueda.

Se identifican dos dificultades principales:

1. Espacio de Búsqueda Exponencial: Para una fórmula con $n$ variables, existen $2^n$ asignaciones totales posibles. La enumeración explícita es inviable para $n$ grandes. El artículo aboga por asignaciones parciales (implicantes) para representar conjuntos de asignaciones totales, comprimiendo así el espacio de soluciones.
2. Cláusulas de Bloqueo y Memoria: Los solucionadores AllSAT tradicionales basados en Aprendizaje de Cláusulas Impulsado por Conflictos (CDCL) y Retroceso No Cronológico (NCB) dependen de añadir cláusulas de bloqueo para evitar el redescubrimiento del mismo modelo. A medida que crece el número de modelos, el número de cláusulas de bloqueo puede volverse exponencial, lo que provoca desbordamientos de memoria y un rendimiento degradado de la propagación unitaria.
3. Proyección: En muchas aplicaciones (por ejemplo, convertir fórmulas no-CNF mediante transformación de Tseitin), es necesario enumerar soluciones solo para un subconjunto de variables "importantes" ($V_r$), ignorando las variables auxiliares "irrelevantes" ($V_i$).

El artículo se centra en la enumeración disjunta, donde las asignaciones repetidas están estrictamente prohibidas, un requisito para aplicaciones como la Integración de Modelos Ponderados (WMI) y la inferencia probabilística.

Metodología

Los autores proponen dos solucionadores novedosos: TabularAllSAT (para lógica proposicional) y TabularAllSMT (para SMT). Ambos integran CDCL con Retroceso Cronológico (CB) para eliminar la necesidad de cláusulas de bloqueo mientras se mantiene la disyunción.

1. Algoritmo Central de Búsqueda (CDCL + CB)

El bucle de búsqueda combina las fortalezas de CDCL (escapar de regiones insatisfacibles mediante análisis de conflictos) y CB (exploración sistemática sin cláusulas de bloqueo redundantes).

• Manejo de Conflictos: Cuando se detecta un conflicto, el solucionador realiza un análisis de conflicto estándar para derivar una cláusula de conflicto. Sin embargo, en lugar de retroceder no cronológicamente al nivel de la cláusula de conflicto (como en CDCL estándar), el solucionador retrocede cronológicamente a la literal de decisión asignada más recientemente e invierte su valor.
• Bloqueo Implícito: Para garantizar la disyunción sin almacenar cláusulas de bloqueo explícitas, el solucionador utiliza cláusulas de razón de retroceso virtuales. Cuando se encuentra un modelo y se invierte una literal de decisión, la razón del cambio se registra como Backtrue. Esto define implícitamente una cláusula de bloqueo que consiste en la negación de todas las literales de decisión hasta ese punto.
• Terminación: La búsqueda termina cuando el solucionador retrocede al nivel de decisión 0, asegurando que todo el espacio ha sido escaneado sistemáticamente sin repeticiones.

2. Reducción Cronológica de Implicantes

Un componente crítico es la reducción de asignaciones totales en asignaciones parciales compactas (implicantes). El artículo introduce dos algoritmos:

• Reducción Conservadora (Línea Base): Basada en literales vigilados por 2, este algoritmo verifica si una literal es necesaria para que la asignación parcial actual satisfaga la fórmula. Respeta el orden de decisión y las banderas Backtrue para garantizar la disyunción.
• Reducción Agresiva (Novedosa): Este algoritmo simula un ordenamiento de decisiones óptimo. Identifica literales "necesarias" (aquellas requeridas para satisfacer cláusulas específicas) y literales "innecesarias". Permite la eliminación de literales innecesarias independientemente de su nivel de decisión, siempre que no estén marcadas con Backtrue ni involucradas en el análisis de conflictos. Esto se logra mediante:
  1. Contar cuántas literales en cada cláusula están actualmente en la trayectoria.
  2. Eliminar iterativamente literales que no son el único satisfactor de ninguna cláusula.
  3. Reconstruir la trayectoria solo con las literales necesarias, posponiendo efectivamente la asignación de variables innecesarias al final del bucle de búsqueda.

3. Extensiones a Proyección y SMT

• Enumeración Proyectada: El algoritmo se adapta para manejar un subconjunto de variables relevantes ($V_r$). La heurística de decisión prioriza $V_r$ sobre las variables irrelevantes ($V_i$). Durante la reducción de implicantes, las literales correspondientes a $V_i$ se descartan automáticamente, asegurando que la salida contenga solo asignaciones para $V_r$.
• Integración AllSMT: El marco integra un solucionador de teorías (MathSAT5). El bucle de búsqueda incluye una verificación de consistencia T después de la propagación unitaria. Si surge un conflicto de teoría, se analiza de manera similar a un conflicto booleano, y el solucionador retrocede cronológicamente. Los átomos de teoría generados durante la resolución se tratan como variables irrelevantes para efectos de proyección.

Contribuciones Clave

El artículo describe cinco contribuciones principales:

1. Enumeración Parcial Disjunta: Un procedimiento que combina CDCL y Retroceso Cronológico para enumerar modelos parciales disjuntos sin introducir cláusulas de bloqueo.
2. Algoritmos de Reducción de Implicantes: Dos algoritmos (conservador y agresivo) diseñados para minimizar las asignaciones parciales mientras se adhieren estrictamente a las restricciones de disyunción del cálculo subyacente.
3. Extensión de Enumeración Proyectada: Adaptación del solucionador para enumerar solo un subconjunto de variables importantes, manejando las variables auxiliares introducidas durante la transformación a CNF.
4. Extensión SMT: Integración del razonamiento de teorías en el marco de enumeración, habilitando la resolución AllSMT con enumeración parcial disjunta.
5. Evaluación Experimental: Una comparación exhaustiva contra solucionadores de última generación.

Resultados Experimentales

Los autores evaluaron TabularAllSAT y TabularAllSMT en diversos conjuntos de pruebas (3-SAT aleatorio, SATLIB, SMT sintético y fórmulas no-CNF) frente a solucionadores que incluyen MathSAT5, Dualiza, solucionadores basados en BDD y D4+ModelGraph.

• Reducción de Implicantes: El nuevo algoritmo de reducción agresiva redujo significativamente el número de asignaciones parciales generadas en comparación con la línea base conservadora, particularmente en instancias con un alto número de soluciones totales. Aunque incurrió en una sobrecarga ligera en instancias muy pequeñas, mejoró el tiempo de ejecución general en problemas más grandes.
• Rendimiento AllSAT: TabularAllSAT se desempeñó de manera competitiva o superior a la mayoría de los solucionadores (BC, NBC, MathSAT5). Fue superado por herramientas de compilación de conocimiento (BDD, D4+ModelGraph) en conjuntos de pruebas específicos con pocas cláusulas donde la sobrecarga de compilación era baja. Sin embargo, TabularAllSAT demostró una huella de memoria menor y no experimentó tiempos de agotamiento debido al agotamiento de memoria.
• AllSAT Proyectado: En conjuntos de pruebas no-CNF que requieren proyección, TabularAllSAT superó significativamente a MathSAT5 y Dualiza tanto en velocidad como en el número de instancias resueltas. También superó a D4+ModelGraph en conjuntos de pruebas sintéticos más difíciles.
• Rendimiento AllSMT: TabularAllSMT superó a MathSAT5 (el único otro solucionador AllSMT proyectado disponible públicamente) en tareas de enumeración total y enumeración parcial. La ausencia de cláusulas de bloqueo en TabularAllSMT evitó la degradación del rendimiento observada en MathSAT5 a medida que aumentaba la complejidad del problema.

Significado y Afirmaciones

El artículo afirma que el enfoque propuesto ofrece una alternativa superior a la enumeración tradicional basada en cláusulas de bloqueo, particularmente en escenarios que requieren proyección y razonamiento SMT.

• Eficiencia: Al evitar el crecimiento exponencial de las cláusulas de bloqueo, el solucionador mantiene un rendimiento estable de propagación unitaria y evita desbordamientos de memoria.
• Compacidad: El algoritmo de reducción agresiva de implicantes produce asignaciones parciales más compactas, reduciendo el tamaño de la salida y el espacio de búsqueda para los pasos de enumeración posteriores.
• Generalidad: El marco unifica exitosamente CDCL y Retroceso Cronológico tanto para la enumeración proposicional como para la basada en teorías, extendiendo la aplicabilidad de la enumeración disjunta a dominios complejos como la inferencia probabilística y el conteo de modelos sobre teorías de primer orden.

Los autores posicionan su trabajo como una realización práctica del cálculo formal presentado en [17], proporcionando la primera implementación que maneja efectivamente la proyección y SMT sin la sobrecarga de las cláusulas de bloqueo.