Resumen Técnico: Más allá de las Codificaciones Eager: Un Enfoque Agnóstico a la Teoría para la Enumeración de Lemas Teóricos en SMT

1. Declaración del Problema

En la Satisfacibilidad Modulo Teorías (SMT), elevar las técnicas de razonamiento booleano a menudo requiere generar lemas teóricos (T-lema). Estos son cláusulas T-válidas que descartan asignaciones de verdad que son proposicionalmente satisfactorias pero T-inconsistentes.

Mientras que la resolución estándar de SMT genera estos lemas de forma "perezosa" bajo demanda durante la búsqueda, ciertas tareas complejas de SMT —como la extracción de núcleos insatisfactibles mínimos, MaxSMT, y la compilación de T-OBDDs o T-SDDs— requieren el pre-cálculo "eager" (eager) de un conjunto completo de T-lema de antemano.

Las codificaciones "clásicas" eager existentes son insuficientes para este propósito porque:

1. Son específicas de unas pocas teorías simples (por ejemplo, EUF, DL, LRA).
2. No cumplen con la combinación de teorías.
3. A menudo producen números excesivos de lemas innecesarios.

Actualmente, existe una falta de métodos agnósticos a la teoría para enumerar eficientemente conjuntos completos de T-lema para fórmulas arbitrarias, particularmente para aplicaciones de Compilación de Conocimiento (KC) donde la sobrecarga computacional se traslada a una fase fuera de línea para permitir consultas en tiempo polinómico.

2. Metodología

Los autores proponen un marco para enumerar T-lema que es agnóstico a la teoría subyacente. El enfoque se basa en un método de referencia utilizando AllSMT (enumerando todas las asignaciones T-satisfactorias) e introduce tres mejoras ortogonales y composables para mejorar la escalabilidad:

2.1 Línea Base: Enumeración Total AllSMT

El método de referencia (Algoritmo 2) realiza una enumeración total, no proyectada, AllSMT sobre la fórmula de entrada $\phi[\alpha]$. Iterativamente encuentra asignaciones de verdad totales T-satisfactorias, las bloquea y recopila los T-lema aprendidos por el solucionador hasta que la fórmula se vuelve insatisfactoria.

• Limitación: Este enfoque depende de la enumeración de asignaciones totales. Como se demuestra en el Ejemplo 2, una enumeración parcial ingenua puede fallar en generar los T-lema necesarios porque el solucionador podría nunca explorar la asignación total T-inconsistente específica que desencadena un conflicto. Sin embargo, enumerar todas las asignaciones totales a menudo es computacionalmente intratable debido a la explosión combinatoria.

2.2 Mejora 1: Divide y Vencerás (D&C)

Para mitigar el costo de la enumeración total, los autores proponen una estrategia de Divide y Vencerás (Algoritmo 3):

1. Realizar una enumeración parcial AllSMT para descomponer el espacio de búsqueda booleano en un conjunto de asignaciones parciales disjuntas y T-satisfactorias ($M_{\alpha}^p$).
2. Para cada asignación parcial $\mu \in M_{\alpha}^p$, realizar una enumeración total AllSMT sobre la fórmula restringida $\phi \land \mu$.
3. Las enumeraciones totales se ejecutan en paralelo.

• Racional: Esto transforma una única enumeración total grande e intratable en un paso de descomposición más barato más muchas enumeraciones totales más pequeñas y manejables.

2.3 Mejora 2: Enumeración Proyectada

Los autores observan que la inconsistencia T está determinada exclusivamente por la asignación a los átomos de teoría ($\alpha_T$), no a los átomos booleanos ($\alpha_B$).

• Método: Realizar una enumeración AllSMT proyectada solo sobre $\alpha_T$ (Algoritmo 4).
• Base Teórica: El Teorema 1 prueba que proyectar la enumeración sobre los átomos T produce un conjunto completo de T-lema.
• Beneficio: Esto reduce drásticamente la dimensión de búsqueda. Una única asignación T-satisfactoria sobre $\alpha_T$ representa hasta $2^k$ asignaciones totales sobre el conjunto completo de átomos (donde $k$ es el número de átomos booleanos), reduciendo significativamente el uso de memoria y el tamaño de las cláusulas de bloqueo.

2.4 Mejora 3: Particionamiento Impulsado por la Teoría

Si el conjunto de átomos en $\phi$ puede particionarse en conjuntos disjuntos ($\alpha_1, \dots, \alpha_n$) de tal manera que ningún átomo en un conjunto comparte variables o símbolos no interpretados con átomos en otro, el problema puede descomponerse aún más (Algoritmo 5).

• Método: Basado en la Propiedad 1 y el Teorema 2, los T-lema pueden enumerarse independientemente para cada partición. El algoritmo particiona iterativamente los átomos, enumera lemas para cada partición proyectada sobre los átomos de dicha partición, y acumula los resultados.
• Beneficio: Esto permite la descomposición de una única enumeración total en $n$ enumeraciones proyectadas independientes, ofreciendo aceleraciones exponenciales potenciales para problemas con componentes disjuntos.

3. Contribuciones Clave

1. Marco Agnóstico a la Teoría: La primera presentación explícita de métodos para enumerar conjuntos completos de T-lema para teorías arbitrarias, superando las codificaciones eager específicas de teoría.
2. Técnicas de Escalabilidad: La introducción de tres técnicas ortogonales:
   • Divide y Vencerás: Paraleliza la búsqueda descomponiendo el espacio booleano.
   • Enumeración Proyectada: Reduce la dimensionalidad de búsqueda al centrarse en los átomos T.
   • Particionamiento: Explota la disjunción estructural en la fórmula para resolver subproblemas independientemente.
3. Garantías Teóricas: Pruebas formales (Teoremas 1 y 2) que demuestran que estas optimizaciones preservan la completitud del conjunto de T-lema requerido para descartar todas las asignaciones T-inconsistentes.
4. Integración con Compilación de Conocimiento: El trabajo sirve como una técnica habilitadora para elevar los métodos de Compilación de Conocimiento (específicamente Diagramas de Decisión como OBDDs y SDDs) al nivel de SMT, abordando el cuello de botella previo de la enumeración de T-lema.

4. Resultados Experimentales

Las técnicas fueron evaluadas en dos conjuntos de pruebas:

• Instancias sintéticas SMT(LRA): 450 problemas generados aleatoriamente de [16].
• Instancias de Planificación Temporal: 90 codificaciones SMT de problemas de planificación del dominio "Pintor".

Métricas de Rendimiento:

• Eficiencia Temporal:
• En las pruebas sintéticas, D&C mejoró el rendimiento en hasta 2 órdenes de magnitud sobre la línea base, resolviendo 17 problemas más dentro del tiempo límite.
• Añadir Proyección mejoró aún más los resultados, resolviendo 30 problemas más que solo D&C y reduciendo drásticamente el tiempo para instancias resueltas previamente.
• Particionamiento no mostró mejora en datos sintéticos (ya que pocos problemas tenían particiones disjuntas) pero fue altamente efectivo en problemas de planificación.
• En problemas de planificación, el Particionamiento fue el factor dominante, permitiendo la resolución de problemas con horizonte 5 que anteriormente eran intratables, logrando aceleraciones de varios órdenes de magnitud.
• Número de Lemas:
• D&C tendió a producir ligeramente más lemas debido a la redundancia paralela.
• La Proyección y el Particionamiento generalmente redujeron el número de lemas enumerados al mitigar la exploración redundante y generar lemas más fuertes y pequeños.
• Tamaño del Lema:
• El particionamiento en problemas de planificación resultó en T-lema significativamente más pequeños (menos literales), probablemente debido al recorte temprano de ramas T-inconsistentes que involucraban solo particiones específicas.

5. Significado y Afirmaciones

El artículo afirma que estas técnicas mejoran drásticamente la eficiencia y la escalabilidad de la enumeración de T-lema en comparación con el enfoque AllSMT de línea base.

• Rol Habilitador: El significado principal es habilitar la aplicación práctica de la Compilación de Conocimiento a SMT. Los autores notan que en su trabajo anterior [16], la enumeración de T-lema fue el "principal cuello de botella" para compilar Diagramas de Decisión. Al resolver este cuello de botella, los métodos propuestos allanan el camino para escalar estas técnicas de compilación a instancias complejas del mundo real.
• Modestia: Los autores tienen cuidado de señalar que las mejoras dependen del contexto. Por ejemplo, la proyección no ayudó con los problemas de planificación porque las asignaciones de átomos T eran consecuencias deterministas de las asignaciones booleanas en esas codificaciones específicas. De manera similar, el particionamiento solo produjo beneficios cuando la estructura del problema permitía naturalmente particiones disjuntas.

En resumen, el artículo proporciona un conjunto de herramientas robusto y agnóstico a la teoría para la enumeración eager de T-lema, transformando un paso previamente intratable en un proceso escalable, facilitando así aplicaciones avanzadas de SMT como MaxSMT y Compilación de Conocimiento.