Resumen Técnico: Tableaux de Modal CEGAR con RECAR y Atajos de Resolución basados en SAT

Planteamiento del Problema

El artículo aborda el desafío de decidir eficientemente la satisfacibilidad en la lógica multimodal $K_n$ (también conocida como $\mathcal{ALC}$). Aunque los tableaux de CEGAR (Counter-Example Guided Abstraction Refinement) han demostrado ser altamente efectivos para problemas insatisfacibles y muchos problemas de satisfacibilidad, presentan dificultades con instancias de satisfacibilidad de gran tamaño. Específicamente, la implementación previa de los autores, CEGARBox, superó a otros solvers en benchmarks estándar, pero perdió ante el probador de resolución modal KSP en el conjunto de benchmarks MQBF. El problema central identificado es que los tableaux de CEGAR construyen explícitamente modelos que satisfacen la fórmula; para problemas con altos factores de ramificación, esto puede llevar a la generación de modelos exponencialmente grandes, causando tiempos de espera agotados (timeouts). A diferencia de los métodos basados en resolución (como KSP), que pueden determinar la satisfacibilidad mediante la saturación sin construir un modelo completo, los tableaux de CEGAR carecen de un "atajo ESAT" efectivo (un mecanismo para confirmar rápidamente la satisfacibilidad sin la construcción completa del modelo).

Metodología

Los autores investigan dos enfoques distintos para integrar atajos ESAT en los tableaux de CEGAR, implementados en un nuevo sistema en C++ llamado CEGARBox++. Ambos enfoques utilizan una estructura de datos Trie para almacenar cláusulas modales en Forma Normal Clausal Modal Separada (SNFmc).

1. El enfoque RECAR (RECARTAB)

Este método adapta el marco de trabajo RECAR (Recursive Explore and Check Abstraction Refinement), propuesto originalmente por Lagniez et al. para CEGAR general.

• Mecanismo: En lugar de crear un mundo separado para cada cláusula diamante disparada (lo que conduce a una ramificación exponencial), RECARTAB intenta agrupar múltiples cláusulas diamante en un único mundo sucesor utilizando una sobre-aproximación. Etiqueta las cláusulas diamante con etiquetas e intenta satisfacer una conjunción de sus objetivos en un solo mundo.
• Refinamiento: Si surge un conflicto que involucra múltiples diamantes, el algoritmo los separa asignando etiquetas nuevas y reinicia la búsqueda.
• Objetivo: Encontrar un modelo más pequeño (menos mundos) que el enfoque CEGAR estándar, evitando así la explosión exponencial en la generación de mundos.

2. El enfoque de Oráculo basado en Resolución (CEGARBox++(KSP))

Este novedoso enfoque integra el probador de teoremas de resolución modal KSP como un oráculo para detectar "puntos fijos" en la búsqueda de CEGAR.

• Mecanismo: El sistema ejecuta CEGARBox++ y KSP en paralelo (multihilo). KSP opera sobre un Trie lineal (SNFml) y realiza resolución desde la capa modal más profunda hacia la raíz.
• Detección de punto fijo: Cuando KSP satura completamente una capa modal $l$ con respecto a la capa $l+1$, emite cláusulas clásicas aprendidas. CEGARBox++ importa estas cláusulas. Si una capa está saturada (se alcanza un "punto fijo"), CEGARBox++ infiere que no es posible realizar más refinamientos (aprendizaje de nuevas cláusulas) para esa capa.
• Atajo: Al detectar un punto fijo, CEGARBox++ se salta el proceso costoso de generar mundos sucesores (la regla de "salto") para esa capa y devuelve inmediatamente Satisfacible, apoyándose en el lema de que si la sub-aproximación es un punto fijo, la fórmula modal completa es satisfacible.

Contribuciones Clave

1. Implementación de CEGARBox++: Una nueva implementación en C++ de tableaux de CEGAR que sirve como base para los experimentos.
2. Algoritmo RECARTAB: Una extensión sólida y completa de los tableaux de CEGAR que incorpora atajos ESAT de estilo RECAR para intentar la minimización del modelo.
3. Integración CEGARBox++(KSP): La primera integración efectiva de métodos de SAT, tableaux y resolución para la satisfacibilidad modal. Utiliza KSP no solo como un compañero de portafolio, sino como un oráculo interno para detectar puntos fijos y activar la terminación temprana para problemas de satisfacibilidad.
4. Análisis Teórico: Pruebas formales de corrección (soundness), completitud y terminación para ambos enfoques, tanto el basado en RECAR como el basado en resolución.

Resultados Experimentales

Los autores evaluaron sus enfoques en los benchmarks estándar K (LWB-K, 3CNF y MQBF) utilizando una CPU Intel i7-11700F.

• Rendimiento de RECAR: Se encontró que el enfoque RECARTAB (RECARBox) no es competitivo. Generalmente funcionó peor que el CEGARBox++ estándar. Los autores lo atribuyen a la sobrecarga de buscar modelos más pequeños; si un modelo más pequeño no existe o es difícil de encontrar, el cómputo adicional se desperdicia.
• Rendimiento basado en Resolución: CEGARBox++(KSP) demostró un rendimiento superior:
  • Superó significativamente tanto a CEGARBox++ independiente como a KSP independiente en los benchmarks MQBF (que están dominados por problemas de satisfacibilidad).
  • Logró aceleraciones de hasta 100x en ciertas instancias de satisfacibilidad en comparación con KSP por sí solo.
  • En los benchmarks 3CNF, funcionó de manera equivalente a CEGARBox++.
  • En los benchmarks LWB-K, fue ligeramente superado por CEGARBox++ solo, probablemente debido a la sobrecarga de la generación de la forma normal de KSP, que produce más cláusulas para fórmulas masivas.
• Sinergia vs. Paralelismo: Los autores descartaron la posibilidad de que las ganancias de rendimiento se debieran simplemente al paralelismo (duplicación de recursos). CEGARBox++(KSP) resolvió problemas de satisfacibilidad que KSP solo no pudo, demostrando que el componente CEGAR contribuyó activamente a la solución al proporcionar el contexto necesario al probador de resolución o al podar el espacio de búsqueda mediante la detección de puntos fijos.

Significancia y Reivindicaciones

El artículo afirma que CEGARBox++(KSP) representa la primera integración efectiva de métodos de SAT, tableaux y resolución para la satisfacibilidad modal que funciona mejor que sus componentes individuales.

• Superación de Limitaciones: El trabajo aborda la debilidad fundamental de los tableaux de CEGAR al manejar grandes problemas de satisfacibilidad mediante la introducción de un mecanismo para detectar cuándo existe un modelo sin construirlo explícitamente.
• Fortalezas Complementarias: Los resultados resaltan que, mientras que los solvers basados en SAT, basados en tableaux y basados en resolución han sido tradicionalmente métodos competidores con diferentes fortalezas (ej. tableaux para insatisfacibilidad, resolución para satisfacibilidad), su integración puede dar lugar a un solver que es "mayor que la suma de sus partes".
• Perspectiva Futura: Los autores señalan modestamente que su implementación actual es ingenua (utilizando E/S de archivos para la comunicación y la forma normal específica de KSP). Sugieren que una integración más pulida, que potencialmente utilice la propia generación de forma normal de CEGAR y mejores protocolos de comunicación, podría permitir que este enfoque híbrido supere a los solvers existentes en todos los conjuntos de benchmarks, incluyendo los LWB-K donde actualmente queda rezagado.

El artículo concluye que, si bien el enfoque RECAR no tuvo éxito en este contexto, la estrategia de detección de puntos fijos utilizando un oráculo de resolución es una dirección prometedora para los algoritmos CEGAR recursivos, particularmente aquellos que involucran ramificación.