On Proof Systems for #QBF

Título: Sobre los sistemas de prueba para #QBF

Planteamiento del problema
El artículo aborda el problema #QBF, que consiste en computar el número de estrategias ganadoras para el jugador existencial en una Fórmula Booleana Cuantificada (QBF). Este problema se identifica como #PSPACE-completo, lo que lo hace computacionalmente más difícil que el problema análogo de #SAT (conteo de modelos para fórmulas proposicionales), donde el número de soluciones es como máximo exponencial. En contraste, el número de estrategias ganadoras en #QBF puede ser doblemente exponencial. Si bien se han estudiado sistemas de prueba para #SAT (por ejemplo, KCPS, CPOG, CLIP, MICE) y para QBF (por ejemplo, ∀Exp), existe una falta de sistemas de prueba dedicados para el problema general de #QBF capaces de certificar el conteo de estrategias ganadoras. Los solvers existentes como d4-QBF y qCounter existen, pero carecen de un marco de complejidad de prueba formalizado para la certificación.

Metodología
Los autores extienden conceptos tanto de los sistemas de prueba de QBF como de los sistemas de prueba de #SAT para diseñar nuevos sistemas de prueba para #QBF. Exploran tres enfoques distintos:

1. Sistema Naive (Ingenuo): Un sistema rudimentario que enumera todas las $k$ estrategias ganadoras. Certifica el conteo probando la corrección de cada estrategia (mediante pruebas de tautología de funciones de Skolem), probando la distinción de las estrategias (mediante asignaciones de testigos) y probando la inexistencia de cualquier otra estrategia (mediante una codificación de QBF falsa). Los autores señalan que este sistema sufre de cotas inferiores triviales cuando el número de estrategias es doblemente exponencial.
2. Sistema basado en expansión (∀Exp+MICE): Este enfoque adapta la regla de ∀-expansión utilizada en la resolución de QBF. Expande semánticamente la QBF sobre todas las posibles asignaciones a las variables universales, transformando el problema #QBF en un problema #SAT. La CNF resultante es procesada mediante el sistema de prueba de #SAT llamado MICE. Los autores argumentan que este sistema requiere inherentemente un tamaño exponencial relativo al número de variables universales porque debe expandir todas las asignaciones universales para preservar el conteo de modelos.
3. Sistema basado en líneas (Q-MICE): La principal contribución es la propuesta de Q-MICE (Inducción por Extensión de Reclamaciones de Conteo de Modelos Cuantificados). Inspirado en el sistema MICE para #SAT, Q-MICE es un sistema de prueba basado en líneas donde cada línea es una reclamación de la forma $(Q.F, A, c)$.
   • $Q.F$: Una QBF verdadera.
   • $A$: Una estrategia parcial que consiste en funciones de Skolem para un subconjunto de variables existenciales.
   • $c$: El número de formas de extender $A$ en estrategias ganadoras completas.
   • Reglas de inferencia: Q-MICE utiliza tres reglas principales:
     • Regla de Axioma: Deriva reclamaciones para QBFs restringidas donde la matriz es una tautología, permitiendo el conteo combinatorio directo de las extensiones.
     • Reglas de Composición: Permiten combinar o simplificar reclamaciones. Composición-a suma estrategias completas distintas; Composición-b elimina las restricciones de la estrategia cuando la unicidad es probada; Composición-c combina reclamaciones donde las estrategias difieren solo en variables específicas, siempre que una prueba de "ausencia de modelos" certifique que no existen otras estrategias.
     • Regla de Unión (Join Rule): Combina dos reclamaciones que difieren solo por una restricción en una variable universal, multiplicando sus conteos, siempre que la estructura del árbol de asignación lo permita (grafos de camino).

Contribuciones clave y resultados

• Formalización de Q-MICE: El artículo define Q-MICE y demuestra que es sano y completo (Teorema 16). Es verificable en tiempo polinómico.
• Separación Exponencial: Los autores demuestran que Q-MICE es exponencialmente más fuerte que tanto el sistema naive como el sistema ∀Exp+MICE (Teorema 17).
  • Familia XOR-PAIRS: Introducen una versión cuantificada de la fórmula proposicional XOR-PAIRS. Mientras que esta familia requiere pruebas superpolinómicas (exponenciales) en ∀Exp+MICE debido a la necesidad de expandir las variables universales, Q-MICE proporciona una prueba de longitud constante y tamaño polinómico utilizando las reglas de Axioma y Composición-b.
  • Familia de QBF Afín Indexado: Construyen una familia de QBFs que representan un proceso de cifrado simple. Esta familia tiene $2^n$ estrategias ganadoras, lo que requiere pruebas exponenciales tanto en los sistemas naive como en ∀Exp+MICE. Q-MICE maneja esto con una prueba de longitud lineal y tamaño polinómico, aplicando iterativamente las reglas de composición y unión.
• Análisis Estructural: El artículo destaca que los sistemas basados en expansión sufren de debilidades estructurales inherentes (explosión exponencial) al tratar con variables universales, mientras que Q-MICE entrelaza el manejo de cuantificadores con el conteo para mantener la eficiencia.

Significancia y Reclamaciones
El artículo afirma que la existencia de sistemas de prueba como Q-MICE es crucial para avanzar en la teoría de #QBF y para certificar la corrección de los solvers de #QBF, un área que se encuentra actualmente en sus primeras etapas. Al proporcionar un marco para certificar los conteos de modelos sin enumerar todas las estrategias, Q-MICE ofrece un camino hacia una verificación de solvers más robusta.

Los autores señalan modestamente que, aunque Q-MICE es potente, aún no incorpora las reglas de descomposición presentes en los solvers de vanguardia como d4-QBF, aunque sugieren que esto podría añadirse como una regla de inferencia modular. También identifican problemas abiertos, incluyendo el establecimiento de cotas inferiores genuinas para Q-MICE (conjeturando que el XOR-PAIRS proposicional podría ser difícil para este, aunque esto no es aún una cota inferior probada) y la extensión de otros sistemas de prueba de #SAT (CPOG, CLIP, KCPS) al dominio de #QBF. El artículo no propone nuevos solvers experimentales, sino que se enfoca estrictamente en la complejidad de prueba teórica y la separación de estos sistemas.