Resumen Técnico: Cálculo de Implicantes SAT Cortos Mediante Codificaciones Ising/QUBO

1. Enunciado del Problema

Muchas tareas de razonamiento, incluyendo la explicación, el diagnóstico y la compresión de modelos, requieren asignaciones parciales satisfactorias cortas (implicantes) en lugar de asignaciones totales. En estos contextos, las variables no asignadas actúan como verdaderos "indiferentes", y a menudo solo un subconjunto de variables (variables visibles) es semánticamente relevante, mientras que otras sirven como soporte oculto.

Aunque los solucionadores SAT modernos calculan eficientemente asignaciones satisfactorias totales, derivar implicantes cortos típicamente requiere llamadas repetidas a SAT o un post-procesamiento dedicado. De manera similar, las formulaciones estándar de SAT a Ising/QUBO son inherentemente limitadas: mapean fórmulas CNF a funciones de energía cuadráticas donde los estados fundamentales corresponden a asignaciones totales. El modelo Ising/QUBO asigna un valor a cada espín, careciendo de una representación nativa para variables "no asignadas". En consecuencia, el cálculo de implicantes cortos ha sido históricamente dejado a algoritmos externos en lugar de ser capturado dentro del propio modelo de optimización cuadrática.

2. Metodología

Los autores proponen un marco de optimización unificado que soporta nativamente asignaciones parciales de tres valores (Verdadero, Falso, No asignado) dentro de un modelo cuadrático Ising/QUBO.

2.1 Representación de Doble Polaridad

Para representar variables no asignadas, el marco introduce una codificación de doble polaridad. Para cada variable proposicional $A_i$, se utilizan dos espines binarios $(p_i, n_i)$:

• $(1, 0) \implies A_i = \top$
• $(0, 1) \implies A_i = \bot$
• $(0, 0) \implies A_i$ está no asignada (indiferente)
• $(1, 1) \implies$ Inconsistente (prohibido)

Se añade una penalización de consistencia semántica $M \cdot p_i n_i$ para prohibir el estado inconsistente.

2.2 Codificación de Cláusulas

Las cláusulas se codifican utilizando funciones de penalización cuadráticas estándar. Para una cláusula $C_k = (\ell_1 \lor \ell_2 \lor \ell_3)$, los literales se mapean a sus espines de polaridad correspondientes. Para mantener la forma cuadrática, se introduce una variable auxiliar $c_k$ para capturar la condición donde los dos primeros literales son falsos. La función de energía penaliza las configuraciones donde todos los literales son falsos (es decir, donde todos los espines correspondientes son 0).

2.3 Esparsidad y Función Objetivo

Se añade un término de esparsidad a la función de energía: $E_{sparse} = \gamma \sum (p_i + n_i)$. Este término penaliza los espines activos, sesgando al optimizador hacia configuraciones con menos variables asignadas (implicantes más cortos).
La función de energía total es:
$$E_F = \sum M p_i n_i + \sum E_{clause}(k) + \gamma \sum (p_i + n_i)$$

2.2 Regímenes de Peso

El artículo establece condiciones teóricas sobre los pesos ($\lambda$ para penalizaciones de cláusulas, $M$ para consistencia, $\gamma$ para esparsidad) para garantizar la corrección. Específicamente, si $\lambda > n\gamma$ y $M > n\gamma$ (donde $n$ es el número de variables), los estados fundamentales de la función de energía corresponden exactamente a implicantes de cardinalidad mínima.

2.5 Reducción y Proyección

• Reducción de Implicantes: Dada una asignación satisfactoria total, el marco restringe el espacio de búsqueda fijando los espines de polaridad "opuesta" a 0. Esto permite que el optimizador solo elimine literales de la asignación existente, encontrando la sub-asignación más corta que sigue siendo un implicante válido.
• Proyección: Para centrarse en un subconjunto de variables visibles $P$, la penalización de esparsidad se aplica solo a las variables en $P$. Las variables ocultas $H$ permanecen sin restricciones por esparsidad, actuando como soporte auxiliar libre. Esto permite que el modelo encuentre asignaciones cortas sobre $P$ mientras satisface la fórmula mediante $H$.

3. Contribuciones Clave

1. Codificación Nativa de Tres Valores: Una codificación SAT a Ising/QUBO que representa nativamente asignaciones parciales (Verdadero/Falso/No asignado) mediante semántica de doble polaridad, eliminando la necesidad de post-procesamiento externo para interpretar estados "no asignados".
2. Variantes de Objetivo Flexibles: Formulaciones QUBO donde la reducción de implicantes se logra mediante restricciones de polaridad y la proyección se logra restringiendo las penalizaciones de esparsidad a variables visibles, todo dentro de una única estructura de modelo cuadrático fijo.
3. Garantías Teóricas: Identificación de regímenes de peso específicos ($\lambda > n\gamma, M > n\gamma$) que garantizan que los estados fundamentales correspondan a implicantes de cardinalidad mínima. El artículo proporciona un criterio para reconocer implicantes válidos directamente desde el valor final de energía.
4. Validación Empírica: Una evaluación utilizando recocido simulado en fórmulas 3-SAT aleatorias y fórmulas no-CNF, demostrando la capacidad de la codificación para producir asignaciones parciales cortas y lograr minimalidad mediante refinamiento iterativo.

4. Resultados Experimentales

Los autores evaluaron la codificación utilizando Recocido Simulado (SA) en dos conjuntos de referencia:

• 3-SAT Aleatorio: Instancias satisfacibles con baja densidad de cláusulas por variable ($m/n = 1.5$).
• Fórmulas No-CNF: Fórmulas booleanas convertidas a CNF mediante transformaciones Tseitin/Plaisted-Greenbaum, creando un escenario proyectado con variables auxiliares ocultas.

Hallazgos Clave:

• Compacidad: En 3-SAT aleatorio, la codificación deja aproximadamente un tercio de las variables no asignadas en promedio mientras preserva la satisfacibilidad.
• Minimalidad: Mientras que el SA de línea base a menudo encuentra asignaciones de cardinalidad mínima en instancias pequeñas a medianas, las tasas de éxito disminuyen a medida que crece el tamaño del problema debido a mínimos locales. Sin embargo, el refinamiento iterativo (congelar la mejor solución y volver a ejecutar SA para reducir aún más) mejora significativamente los resultados.
• Minimalidad vs. Cardinalidad Mínima: El refinamiento iterativo logra minimalidad por inclusión (implicantes primos) con alta probabilidad. Lograr cardinalidad mínima (tamaño global mínimo) es más difícil pero se observa frecuentemente, particularmente en referencias no-CNF donde la estructura permite completaciones ocultas uniformes.
• Escenario Proyectado: En el modo proyectado, el método recupera con éxito asignaciones de cardinalidad mínima sobre variables visibles, incluso con una alta proporción de variables auxiliares ocultas (65–70% del total de variables).

5. Significado y Afirmaciones

El artículo afirma que este marco ofrece un enfoque de optimización unificado para calcular asignaciones parciales cortas, reemplazando la necesidad de subrutinas de reducción externas en pipelines de AllSAT o explicación.

• Significado Teórico: Cierra la brecha entre la naturaleza de "asignación total" de los modelos Ising y los requisitos de "asignación parcial" de muchas tareas de razonamiento mediante la introducción de una representación de doble polaridad con regímenes de peso demostrables para la minimalidad.
• Significado Práctico: La codificación sirve como un "reemplazo directo" para los pasos de reducción en flujos de trabajo existentes. Los autores enfatizan que el enfoque es robusto bajo backends de optimización genéricos (como el Recocido Simulado) y no requiere hardware especializado para demostrar validez semántica, aunque señalan que los recocedores cuánticos o máquinas Ising especializadas podrían potencialmente producir mejores resultados.
• Limitaciones: Los autores reconocen modestamente que, aunque la codificación garantiza estados fundamentales de cardinalidad mínima teóricamente, los optimizadores heurísticos pueden quedar atrapados en mínimos locales. Además, en el escenario proyectado, la codificación impone un "testigo uniforme" (una única asignación oculta para todas las completaciones visibles), que es un requisito más estricto que la semántica estándar de implicantes proyectados, aunque los autores argumentan que esto se cumple para muchas conversiones prácticas no-CNF.

El trabajo se posiciona como una validación semántica de codificaciones cuadráticas para razonamiento parcial, demostrando que con un ajuste adecuado de parámetros y refinamiento iterativo, los modelos Ising/QUBO pueden calcular efectivamente implicantes mínimos y de cardinalidad mínima.