An Efficient Algorithm for Solving the 2-MAXSAT Problem

Resumen Técnico: Un Algoritmo Eficiente para Resolver el Problema 2-MAXSAT

Definición del Problema
El artículo aborda el problema 2-MAXSAT, una versión restringida del problema de Satisfacibilidad Máxima (MAXSAT). Dada una colección $V$ de $m$ variables booleanas y una colección $C$ de $n$ cláusulas en Forma Normal Conjuntiva (CNF), donde cada cláusula contiene como máximo dos literales, el objetivo es encontrar una asignación de verdad que maximice el número de cláusulas satisfechas. El problema se establece como NP-completo, incluso bajo esta restricción.

Metodología
El algoritmo propuesto se aparta de los métodos tradicionales de ramificación y poda (branch-and-bound) o de aproximación al transformar el problema en una tarea de maximización de Forma Normal Disyuntiva (DNF) y utilizar una estructura de búsqueda especializada basada en grafos. La metodología procede en tres etapas principales:

1. Transformación a DNF:
   El algoritmo construye una nueva fórmula $D$ en DNF a partir de la fórmula CNF original $C$. Para cada cláusula $C_i = l_{i1} \lor l_{i2}$ en $C$, el algoritmo introduce una nueva variable auxiliar $x_i$ y genera dos conjunciones: $D_{i1} = l_{i1} \land x_i$ y $D_{i2} = l_{i2} \land \neg x_i$. La fórmula resultante $D$ consta de $2n$ conjunciones. La Proposición 1 en el artículo establece que $C$ tiene al menos $n^*$ cláusulas satisfechas si y solo si $D$ tiene al menos $n^*$ conjunciones satisfechas bajo una asignación de verdad para $V \cup \{x_1, \dots, x_n\}$.

2. Representación en Grafos (p-grafos y Tries):*
   Para representar eficientemente las asignaciones de verdad que satisfacen las conjunciones en $D$, el artículo introduce el p-grafo*.

   • Secuencias de Variables: Cada conjunción se convierte en una secuencia de variables ordenada basada en la frecuencia global de aparición de las variables. Los literales negativos se manejan introduciendo una notación especial $(c, *)$, que representa que la variable $c$ puede ser verdadera o falsa (o saltada) sin afectar la veracidad de la conjunción.
   • p-grafos: Un grafo dirigido que representa una sola conjunción donde los nodos corresponden a las variables en la secuencia. Los "espacios" (aristas que saltan variables) representan las opciones $(c, *)$.
   • p-grafos:* Un refinamiento de los p-grafos donde los "espacios superpuestos" (variables opcionales consecutivas) se fusionan mediante el cierre transitivo. Esto asegura que el grafo represente correctamente todas las asignaciones de verdad válidas para una conjunción específica.
   • Estructura tipo Trie ($G$): Todos los p*-grafos se integran en un único grafo de tipo trie $G$. Esta estructura agrupa secuencias de variables comunes para evitar comprobaciones redundantes. El grafo incluye "nodos de ramificación" donde los caminos divergen.

3. Búsqueda Recursiva Bottom-Up:
   El núcleo del algoritmo, SEARCH(G), explora el grafo $G$ de manera ascendente (post-orden) para encontrar el subconjunto máximo de conjunciones satisfechas.

   • Subconjuntos Alcanzables (RS): Para un nodo de ramificación $v$, el algoritmo calcula los "subconjuntos alcanzables" de los nodos alcanzables mediante espacios desde los ancestros. Estos subconjuntos representan grupos de conjunciones que pueden satisfacerse simultáneamente al omitir ciertas variables.
   • Límites Superiores (upBounds): Basándose en los RS, el algoritmo identifica "límites superiores" (upper boundaries), que son conjuntos de nodos que permiten la fusión de subgrafos.
   • Construcción Recursiva: Cuando se encuentra un nodo de ramificación, el algoritmo construye un nuevo subgrafo más pequeño de tipo trie con raíz en los nodos del límite superior. Se añade una raíz virtual (el nodo de ramificación original) para mantener la conectividad. El algoritmo llama recursivamente a SEARCH sobre estos subgrafos.
   • Optimización: Para evitar el cómputo redundante, el algoritmo emplea dos mejoras: (1) limitar los cálculos de RS al segmento entre el nodo de ramificación actual y su ancestro de ramificación más bajo, y (2) utilizar un arreglo de hash para cachear los resultados de los subgrafos visitados previamente, suprimiendo llamadas recursivas repetidas.

Contribuciones Clave

• Técnica de Transformación: Una reducción en tiempo polinomial del problema 2-MAXSAT a un problema de máxima conjunción satisfactoria en DNF.
• Estructura de p-grafo:* La definición de p*-grafos y su cierre transitivo para representar de manera precisa y compacta las asignaciones de verdad para conjunciones que contienen variables opcionales.
• Búsqueda Recursiva en Trie: Un novedoso algoritmo de búsqueda que construye y busca dinámicamente una estructura de grafo tipo trie, utilizando "subconjuntos alcanzables" y "límites superiores" para fusionar los espacios de solución de manera eficiente.
• Análisis de Complejidad: El artículo proporciona un análisis detallado alegando que el algoritmo opera dentro de límites de tiempo polinomial.

Resultos y Complejidad
El artículo afirma que la complejidad de tiempo en el peor de los casos del algoritmo propuesto está acotada por $O(n^2 m^4)$, donde $n$ es el número de cláusulas y $m$ es el número de variables.

• La construcción del trie inicial y los p*-grafos toma $O(nm^2)$.
• La búsqueda recursiva involucra como máximo $O(nm)$ nodos de ramificación.
• Cada nodo de ramificación está involucrado en como máximo $O(m)$ llamadas recursivas debido a la reducción de la altura del grafo en cada paso.
• El costo de construir un subgrafo por llamada es $O(nm^2)$.
• Combinando estos factores, se obtiene el límite $O(n^2 m^4)$.

Significancia y Reivindicaciones
El artículo concluye que, dado que el problema 2-MAXSAT es conocido por ser NP-completo, la existencia de un algoritmo de tiempo polinomial para resolverlo constituye una prueba de que P = NP. Los autores afirman que este resultado proporciona una prueba de P = NP, alterando fundamentalmente la comprensión de la complejidad computacional para los problemas de satisfacibilidad. El trabajo se presenta como una modificación y extensión de un artículo de conferencia, apoyado por NSERC, Canadá.