Resumen Técnico: Extensión de CDCL a Disyunciones de Ecuaciones de Paridad

Enunciado del Problema

El Aprendizaje de Cláusulas Impulsado por Conflictos (CDCL) es el método dominante para la resolución de SAT, pero está fundamentalmente limitado por el sistema de demostración de Resolución. Los problemas que requieren un tamaño de demostración exponencial en Resolución (como las fórmulas de Tseitin o el principio del palomar biyectivo) son demostrablemente difíciles para CDCL. Aunque algunos solucionadores incorporan fragmentos de sistemas de demostración más potentes —como los solucionadores pseudo-booleanos que utilizan Planos de Corte o los solucionadores CNF-XOR que manejan ecuaciones de paridad—, estos enfoques a menudo tratan el razonamiento de paridad como un módulo separado o se restringen a formas normales específicas (por ejemplo, CNF-XOR).

La brecha específica abordada por este trabajo es la falta de un algoritmo al estilo de CDCL que maneje nativamente fórmulas en XNF (Forma Normal XOR-OR-AND). Las fórmulas XNF consisten en conjunciones de cláusulas lineales, que son disyunciones de ecuaciones de paridad (por ejemplo, $(x \oplus y) \lor \neg(y \oplus z)$). Aunque el sistema de demostración Res(⊕) (Resolución generalizada a XNF) se sabe que es exponencialmente más fuerte que la Resolución para ciertos problemas, los solucionadores existentes no integran completamente el razonamiento Res(⊕) en el bucle de CDCL, ni proporcionan una demostración teórica de que un algoritmo al estilo de CDCL puede simular polinomialmente a Res(⊕).

Metodología

Los autores proponen CDCL(⊕), una generalización del algoritmo CDCL diseñada para operar directamente sobre fórmulas XNF. La metodología se basa en tres componentes centrales:

1. Nuevas Reglas de Inferencia para Res(⊕):
   Los autores introducen una nueva caracterización del sistema de demostración Res(⊕) que reemplaza las reglas estándar de resolución y debilitamiento con suma y cambio de base.

   • Suma: De $C \lor f$ y $D \lor g$, se deduce $C \lor D \lor (f + g)$.
   • Cambio de base: De $C$, se deduce cualquier $D$ tal que $C \equiv D$ (semánticamente equivalente).
     Crucialmente, definen una regla de resolución afín donde las ecuaciones se "aislan" (mediante cambio de base) para permitir la cancelación mediante suma. Esto elimina la necesidad del espacio de búsqueda exponencial asociado con la regla de debilitamiento, permitiendo una simulación polinomial.

2. Propagación de Unidades con Álgebra Lineal:
   A diferencia del CDCL clásico, que propaga basándose en asignaciones de literales, CDCL(⊕) realiza la propagación de unidades utilizando álgebra lineal sobre $\mathbb{F}_2$.

   • El solucionador mantiene un conjunto de unidades conocidas (ecuaciones) $U$.
   • La propagación verifica si una cláusula lineal $C$ implica una nueva ecuación $f$ o una contradicción ($1$) dado $U$.
   • Esto se implementa reduciendo la "negación lineal" de una cláusula (el subespacio de asignaciones que falsifican la cláusula) contra el rango de $U$. Si la negación de la cláusula está contenida dentro del rango de $U$ más una sola ecuación $f$, entonces se deduce $f$.

3. Aprendizaje de Cláusulas mediante Análisis de Conflictos:
   El artículo adapta la estrategia de aprendizaje de cláusulas 1-UIP (Primer Punto de Implicación Único) al entorno XNF. Dado que los grafos de implicación no se traducen directamente a ecuaciones lineales, el algoritmo de aprendizaje opera semánticamente:

   • Comienza con la cláusula de conflicto (la razón de la contradicción).
   • Aplica iterativamente el cambio de base para aislar la ecuación responsable de la decisión más reciente.
   • Aplica la regla de suma para combinar la cláusula aislada con la razón del conflicto, cancelando efectivamente la variable de decisión.
   • Este proceso se repite hasta encontrar una cláusula afirmativa (una cláusula que fuerza una propagación en el nivel de decisión actual).

Contribuciones Clave

Contribuciones Teóricas

• Conexión Bidireccional: El artículo demuestra que CDCL(⊕) no solo produce demostraciones Res(⊕), sino que también simula polinomialmente el sistema de demostración Res(⊕), dadas decisiones no deterministas y reinicios. Esto refleja la relación clásica entre CDCL y Resolución.
• Nueva Caracterización del Sistema de Demostración: Los autores proporcionan un nuevo conjunto de reglas de inferencia (suma y cambio de base) que son polinomialmente equivalentes a Res(⊕) pero carecen de la regla de debilitamiento, lo que las hace adecuadas para la implementación algorítmica.
• Equivalencia de Res(⊕) de Entrada: El artículo demuestra que la propagación de unidades en CDCL(⊕) es equivalente a un fragmento de Res(⊕) conocido como Res(⊕) de entrada, generalizando un resultado conocido para CDCL clásico.
• Factor de Simulación Mejorado: La demostración de simulación mejora el factor polinomial para la relación clásica CDCL/Resolución (igualando el resultado en [7] con un argumento más simple) optimizando cómo se absorben las descomposiciones de cláusulas.

Contribuciones Prácticas

• Implementación Xorcle: Los autores presentan Xorcle, un solucionador de concepto para CDCL(⊕).
  • Implementa álgebra lineal eficiente sobre $\mathbb{F}_2$ utilizando empaquetado de bits.
  • Introduce CSIDS (Suma Decreciente Independiente del Estado de la Cláusula), una nueva heurística para la selección de cláusulas que generaliza VSIDS y CMTF al contexto XNF.
  • Introduce LRUP(⊕), una extensión del formato de registro de demostraciones LRUP para soportar expresiones de paridad.
• Heurísticas para XNF: El artículo detalla adaptaciones para estructuras vigiladas (ciclando a través de cláusulas en lugar de mantener listas de vigilancia complejas debido a dependencias lineales), procedimientos de decisión (ramificándose sobre ecuaciones aleatorias de la negación de una cláusula) y selección de fase (prefiriendo falsificar cláusulas).

Resultados Experimentales

Los autores evaluaron Xorcle en un conjunto de pruebas que incluye:

• Ascon-128: Una familia 2-XNF relacionada con criptografía.
• k-XNFs Aleatorios y Restringidos: Fórmulas sintéticas con números variables de variables y ecuaciones.
• Fórmulas de Tseitin: Problemas de paridad codificados en CNF conocidos por ser difíciles para la Resolución.

Hallazgos Clave:

• Rendimiento en XNF: Xorcle superó a los solucionadores existentes (Kissat, CryptoMiniSAT y 2-Xornado) en pruebas nativas de XNF. Notablemente, superó a 2-Xornado (un solucionador dedicado a 2-XNF) en instancias de Ascon-128 a pesar de utilizar razonamiento XNF general.
• Rendimiento en Fórmulas de Tseitin: En fórmulas de Tseitin codificadas en CNF, Xorcle demostró una escalabilidad casi polinomial en el tiempo de ejecución, mientras que se sabe que los solucionadores basados en Resolución requieren tiempo exponencial. Esto se logró sin preprocesamiento, confiando únicamente en el razonamiento central de CDCL(⊕).
• Calidad de Decisión: Xorcle requirió significativamente menos decisiones que los solucionadores competidores, lo que sugiere que los mecanismos de ramificación y deducción basados en paridad son más efectivos para estas clases de problemas.

Significado y Afirmaciones

El artículo afirma que CDCL(⊕) proporciona el primer marco teórico riguroso e implementación práctica que integra completamente el razonamiento de paridad en el paradigma CDCL.

• Significado Teórico: Establece que las limitaciones de CDCL no son inherentes a la estructura algorítmica, sino al sistema de demostración subyacente (Resolución). Al cambiar a Res(⊕), CDCL puede teóricamente resolver problemas que son exponencialmente difíciles para CDCL estándar.
• Significado Práctico: Los resultados sugieren que la resolución nativa de XNF es viable y potencialmente superior a convertir XNF a CNF o CNF-XOR. La capacidad de resolver fórmulas de Tseitin en tiempo casi polinomial sin preprocesamiento destaca el potencial del razonamiento de paridad para superar las barreras de dureza conocidas en la resolución de SAT.
• Direcciones Futuras: Los autores notan modestamente que Xorcle es un concepto de prueba. Actualmente carece de varias optimizaciones estándar de CDCL (por ejemplo, eliminación de cláusulas, reinicios avanzados, heurísticas dinámicas) y aún no generaliza completamente conceptos como "1-UIP" o "minimización de cláusulas" al entorno semántico XNF. El trabajo abre la puerta a futuras investigaciones sobre heurísticas dirigidas específicamente a fórmulas CNF que requieren implícitamente razonamiento de paridad.