1. La revolución algorítmica silenciosa de la informática

Abra casi cualquier libro de texto de informática teórica y encontrará una advertencia contundente: «El problema de satisfacibilidad booleana (SAT) es NP-completo. Dado que su complejidad temporal en el peor de los casos crece exponencialmente como \(O(2^n)\) con el número de variables \(n\), las instancias grandes son fundamentalmente intratables».

Desde la combinatoria elemental, el argumento parece irrefutable. Una fórmula proposicional sobre \(n = 100\) variables booleanas admite \(2^{100} \approx 1.26 \times 10^{30}\) asignaciones de verdad posibles. Incluso si una supercomputadora pudiera verificar \(10^{12}\) asignaciones por segundo desde el Big Bang (hace 13,800 millones de años), hoy habría explorado menos del \(10^{-8}\) del espacio de búsqueda. De hecho, alrededor de 1990, los mejores solucionadores SAT colapsaban ante fórmulas de apenas \(100\) variables y \(400\) cláusulas.

Sin embargo, en el siglo XXI la ingeniería desafía esa intuición millones de veces al día. Los solucionadores SAT y SMT industriales modernos —como MiniSat, Glucose, Lingeling, CaDiCaL, Kissat y Z3 de Microsoft Research— resuelven rutinariamente instancias de verificación formal de microprocesadores, optimización de compiladores y resolución de dependencias de paquetes con \(10,000,000\) (\(10^7\)) de variables y \(50,000,000\) (\(5 \times 10^7\)) de cláusulas en cuestión de segundos.

Cuando Donald E. Knuth publicó en 2015 el Volumen 4B (Sección 7.2.2.2) de The Art of Computer Programming, dedicó más de 300 páginas exclusivamente a los solucionadores SAT, calificando los avances de finales de los años 90 y principios de los 2000 como una de las mayores revoluciones algorítmicas en la historia de las ciencias de la computación. Si antes reducir un problema a SAT significaba demostrar que era imposible de resolver en la práctica, hoy traducir un problema combinatorio difícil a SAT es la estrategia maestra para resolverlo al instante.

2. Forma Normal Conjuntiva (CNF), transformación de Tseitin y el teorema de Cook-Levin (1971)

2.1 Forma Normal Conjuntiva (CNF) y codificación lineal de Tseitin

Un solucionador SAT opera sobre una fórmula proposicional \(\Phi\) definida sobre \(n\) variables booleanas \(V = \{x_1, \dots, x_n\}\) con valores en \(\{0, 1\}\). Un literal \(\ell \in \{x_v, \neg x_v\}\) es una variable o su negación; una cláusula \(C_i = \bigvee_{j=1}^{k_i} \ell_{i,j}\) es una disyunción (OR lógico, \(\lor\)) de literales; y una fórmula en Forma Normal Conjuntiva (CNF) es una conjunción (AND lógico, \(\land\)) de \(m\) cláusulas:

Si convirtiéramos ingenuamente un circuito lógico arbitrario a CNF aplicando repetidamente la ley distributiva \(A \lor (B \land C) \equiv (A \lor B) \land (A \lor C)\), el tamaño de la fórmula explotaría exponencialmente. En 1968, Grigori Tseitin eliminó esta explosión mediante la transformación de Tseitin: se introduce una nueva variable auxiliar \(y_g\) para la salida de cada compuerta lógica \(g\) del circuito y se codifica la equivalencia local \(y_g \leftrightarrow \text{gate}(a, b)\) con solo 3 o 4 cláusulas. Por ejemplo, una compuerta AND \(y_g \leftrightarrow (a \land b)\) equivale exactamente a tres cláusulas:

De este modo, cualquier circuito con \(|G|\) compuertas se transforma en tiempo y espacio estrictamente lineales \(O(|G|)\) en una fórmula 3-CNF equisatisfacible.

2.2 El teorema de Cook-Levin y el abismo de complejidad entre 2-SAT y 3-SAT

En 1971, Stephen Cook y Leonid Levin demostraron independientemente el teorema de Cook-Levin: todo problema de decisión en la clase \(\text{NP}\) puede reducirse en tiempo polinomial a SAT codificando la tabla de cómputo espacio-temporal de una máquina de Turing no determinista durante \(p(n)\) pasos (estados \(S_{t,q}\), posición del cabezal \(H_{t,i}\), símbolos de cinta \(T_{t,i,\sigma}\)) como una fórmula CNF.

Cuando cada cláusula tiene a lo sumo \(k\) literales (\(k\)-SAT), existe un abismo matemático entre \(k = 2\) y \(k = 3\):

• 2-SAT se resuelve en tiempo lineal \(O(n + m)\): una cláusula binaria \((\ell_1 \lor \ell_2)\) es equivalente a dos implicaciones dirigidas deterministas \((\neg \ell_1 \Rightarrow \ell_2) \land (\neg \ell_2 \Rightarrow \ell_1)\). Construyendo el grafo de implicación sobre los \(2n\) literales, el algoritmo de Tarjan calcula las componentes fuertemente conexas (SCC) en tiempo \(O(n+m)\): la fórmula es satisfacible si y solo si ninguna variable \(x_v\) pertenece a la misma SCC que su negación \(\neg x_v\).
• 3-SAT es NP-completo: una cláusula ternaria \((\ell_1 \lor \ell_2 \lor \ell_3)\) equivale a \((\neg \ell_1 \land \neg \ell_2) \Rightarrow \ell_3\), una hiperarista que requiere dos premisas simultáneas. Bajo la Hipótesis del Tiempo Exponencial (ETH), ningún algoritmo determinista puede resolver 3-SAT en tiempo subexponencial \(2^{o(n)}\) en el peor caso.

3. El algoritmo DPLL clásico (1962) y la tragedia del backtracking cronológico

El algoritmo DPLL (Davis, Putnam, Logemann, Loveland, 1962) combina búsqueda en profundidad con la propagación unitaria (Unit Propagation / Boolean Constraint Propagation, BCP):

Propagación Unitaria (BCP): Si bajo la asignación parcial actual todos los literales de una cláusula \(C = (\ell_1 \lor \dots \lor \ell_{k-1} \lor \ell_k)\) excepto \(\ell_k\) se han evaluado como False (\(0\)) y \(\ell_k\) sigue sin asignar, entonces \(C\) es una cláusula unitaria. El solucionador fuerza inmediatamente \(\ell_k = \text{True}\) (\(1\)) sin ramificar, desencadenando una cascada en dominó de nuevas propagaciones unitarias hasta alcanzar un punto fijo o falsificar por completo alguna cláusula (Conflicto).

¿Por qué DPLL chocaba contra un muro al llegar a unas 100 variables? Por culpa del backtracking cronológico. Si el solucionador asigna \(x_1 = 0\) en el nivel de decisión \(d = 1\), luego toma 48 decisiones totalmente irrelevantes sobre \(x_2, \dots, x_{49}\) en los niveles \(d = 2 \dots 49\), y en el nivel \(d = 50\) asigna \(x_{50} = 1\), provocando un conflicto inmediato causado exclusivamente por \(x_1 = 0\) y \(x_{50}\) a través de las cláusulas \((x_1 \lor \neg x_{50} \lor \pm x_{51})\) y \((x_1 \lor x_{50} \lor \pm x_{52})\), DPLL es ciego a la causa raíz. Retrocede un solo paso al nivel \(d = 49\), invierte la inocente variable \(x_{49}\) y repite exactamente el mismo fracaso a lo largo de \(2^{48} \approx 2.81 \times 10^{14}\) subárboles inútiles (thrashing)!

4. La revolución CDCL: grafos de implicación, resolución 1-UIP y salto atrás

Introducido en GRASP (Marques-Silva & Sakallah, 1996) y perfeccionado en Chaff (Moskewicz et al., 2001), el aprendizaje de cláusulas dirigido por conflictos (CDCL) transformó cada contradicción en un teorema permanente.

  flowchart TD
    Start["Entrada: Fórmula CNF Φ (Nivel de decisión d = 0)"] --> BCP["Propagación de restricciones booleanas (BCP)<br/>Propagación rápida mediante Dos Literales Vigilados (2WL)"]
    BCP --> CheckConflict{"¿Cláusula de conflicto κ<br/>falsificada?"}
    CheckConflict -- "Sin conflicto" --> CheckAllAssigned{"¿Todas las variables<br/>asignadas?"}
    CheckAllAssigned -- "Sí" --> SAT["SATISFACIBLE (SAT)<br/>Devolver asignación σ"]
    CheckAllAssigned -- "No" --> Branch["Ramificación (Decision): d ← d + 1<br/>Elegir variable con máxima actividad VSIDS<br/>Asignar polaridad mediante Phase Saving"]
    Branch --> BCP
    CheckConflict -- "Sí (¡Conflicto!)" --> CheckLevelZero{"¿En nivel raíz<br/>d == 0?"}
    CheckLevelZero -- "Sí" --> UNSAT["INSATISFACIBLE (UNSAT)<br/>Emitir certificado de prueba DRAT"]
    CheckLevelZero -- "No (d > 0)" --> Analyze["Análisis de conflicto (Resolución 1-UIP)<br/>Recorrer el grafo de implicación hacia atrás desde κ<br/>Resolver hasta que quede un único literal del nivel d (First UIP)"]
    Analyze --> Learn["Aprender cláusula e incrementar VSIDS<br/>Añadir C_learned a la base de datos (calcular LBD)<br/>Incrementar actividad VSIDS de las variables resueltas"]
    Learn --> Backjump["Salto atrás no cronológico (Backjump)<br/>Saltar directamente al nivel de aserción d_back (2.º nivel más alto en C_learned)<br/>¡C_learned dispara inmediatamente como cláusula unitaria en BCP!"]
    Backjump --> BCP

4.1 Grafo de implicación, resolución booleana y el Primer Punto de Implicación Único (1-UIP)

Cada literal asignado \(\ell@d\) registra su nivel de decisión \(d\) y su cláusula antecedente (razón) \(\text{reason}(\ell)\). Cuando una cláusula \(\kappa\) resulta falsificada, CDCL inicializa \(C \leftarrow \kappa\) y recorre hacia atrás la pila de asignaciones (Trail) en el nivel actual \(d_{\text{curr}}\), aplicando iterativamente la regla de resolución booleana:

En el grafo de implicación, un vértice \(u@d_{\text{curr}}\) es un Punto de Implicación Único (Unique Implication Point, UIP) si todo camino dirigido desde la decisión \(\ell_{\text{dec}}@d_{\text{curr}}\) hasta el nodo de conflicto \(\Lambda\) pasa obligatoriamente por \(u\) (dominador). El UIP más cercano al conflicto se denomina Primer UIP (First UIP / 1-UIP). Algebraicamente, el bucle de resolución hacia atrás alcanza el 1-UIP en el instante exacto en que la cláusula de trabajo \(C\) contiene un único literal perteneciente al nivel de decisión actual \(d_{\text{curr}}\).

Con \(x_1 = 0@1, x_2 = 0@2, x_3 = 1@3\), la decisión \(x_4 = 1@5\) y las cláusulas \(\omega_1 = (x_1 \lor \neg x_4 \lor x_5)\), \(\omega_2 = (\neg x_4 \lor \neg x_5 \lor x_6)\), \(\omega_3 = (x_2 \lor \neg x_6 \lor x_7)\), \(\omega_4 = (\neg x_3 \lor \neg x_6 \lor x_8)\) que llevan al conflicto \(\kappa = (\neg x_7 \lor \neg x_8)\), al resolver \(\kappa\) con \(\omega_4\) (pivote \(x_8\)) y luego con \(\omega_3\) (pivote \(x_7\)) se obtiene inmediatamente la cláusula aprendida 1-UIP:

4.2 Salto atrás no cronológico (Backjumping) y nivel de aserción

Dado que los niveles en \(C_{\text{learned}}\) son \(\{5, 3, 2\}\), el solucionador salta directamente al segundo nivel de decisión más alto (nivel de aserción) \(d_{\text{back}} = 3\). En el nivel \(3\), \(x_2@2\) y \(\neg x_3@3\) siguen siendo falsos mientras que \(\neg x_6\) queda libre, por lo que \(C_{\text{learned}}\) actúa de inmediato como cláusula unitaria asertiva y fuerza \(\neg x_6 = 1@3\) (\(x_6 = 0@3\)) mediante BCP.

5. Milagros de ingeniería: Dos Literales Vigilados (2WL), VSIDS y LBD

1. Dos Literales Vigilados (Two-Watched Literals, 2WL, Chaff 2001): Como el \(90\%\) del tiempo de CPU se consume en BCP, 2WL explota un invariante genial: mientras una cláusula tenga al menos dos literales no falsificados (sin asignar o verdaderos), jamás podrá convertirse en cláusula unitaria ni en conflicto. El solucionador vigila solo dos literales \(w_1, w_2\) por cláusula. Lo más extraordinario ocurre al hacer backjumping: desasignar variables conserva automáticamente el invariante 2WL, por lo que el retroceso requiere exactamente cero actualizaciones de punteros (\(O(1)\))!
2. VSIDS (Variable State Independent Decaying Sum) y Phase Saving: Cada variable involucrada en la resolución de un conflicto incrementa su puntuación en \(+\Delta\), mientras que \(\Delta \leftarrow \Delta / \gamma\) (\(\gamma = 0.95\)) crece tras cada conflicto, enfocando la búsqueda como un láser en el cuello de botella activo.
3. LBD (Literal Block Distance / Cláusulas «Glue») y reinicios rápidos: Glucose (Audemard & Simon, 2009) define \(\text{LBD}(C)\) como el número de niveles de decisión distintos presentes en una cláusula aprendida \(C\). Las cláusulas con \(\text{LBD} = 2\) (cláusulas de pegamento / Glue Clauses) vinculan directamente el UIP actual con un único bloque pasado y se conservan para siempre.

6. Implementación completa en Python de un motor CDCL

A continuación se muestra una implementación completa y autocontenida en Python de un solucionador CDCL con BCP, grafo de implicación, resolución 1-UIP, salto atrás no cronológico y VSIDS:

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112

from typing import List, Dict, Optional, Set, Tuple

class CDCLSolver:
    '''Minimal Conflict-Driven Clause Learning (CDCL) SAT Solver with 1-UIP & VSIDS.'''
    def __init__(self, num_vars: int, clauses: List[List[int]]):
        self.num_vars = num_vars
        self.clauses: List[List[int]] = [list(set(c)) for c in clauses]
        self.assigns: Dict[int, bool] = {}
        self.trail: List[int] = []
        self.level: Dict[int, int] = {}
        self.reason: Dict[int, Optional[List[int]]] = {}
        self.decision_level: int = 0
        self.activity: Dict[int, float] = {v: 0.0 for v in range(1, num_vars + 1)}
        for c in self.clauses:
            for lit in c:
                self.activity[abs(lit)] += 1.0
        self.var_inc: float = 1.0
        self.var_decay: float = 0.95

    def value_lit(self, lit: int) -> Optional[bool]:
        var = abs(lit)
        if var not in self.assigns:
            return None
        return self.assigns[var] if lit > 0 else not self.assigns[var]

    def assign(self, lit: int, level: int, reason: Optional[List[int]]) -> None:
        var = abs(lit)
        self.assigns[var] = (lit > 0)
        self.trail.append(lit)
        self.level[var] = level
        self.reason[var] = reason

    def bcp(self) -> Optional[List[int]]:
        changed = True
        while changed:
            changed = False
            for clause in self.clauses:
                unassigned_lit = None
                num_unassigned = 0
                satisfied = False
                for lit in clause:
                    val = self.value_lit(lit)
                    if val is True:
                        satisfied = True
                        break
                    elif val is None:
                        num_unassigned += 1
                        unassigned_lit = lit
                if satisfied:
                    continue
                if num_unassigned == 0:
                    return clause
                if num_unassigned == 1 and unassigned_lit is not None:
                    self.assign(unassigned_lit, self.decision_level, clause)
                    changed = True
        return None

    def analyze_conflict(self, conflict_clause: List[int]) -> Tuple[List[int], int]:
        learned: Set[int] = set(conflict_clause)
        def count_curr_level(cset: Set[int]) -> int:
            return sum(1 for lit in cset if self.level[abs(lit)] == self.decision_level)

        idx = len(self.trail) - 1
        while count_curr_level(learned) > 1:
            while True:
                pivot_lit = self.trail[idx]
                idx -= 1
                if -pivot_lit in learned and self.level[abs(pivot_lit)] == self.decision_level:
                    break
            pivot_var = abs(pivot_lit)
            antecedent = self.reason[pivot_var]
            assert antecedent is not None
            self.activity[pivot_var] += self.var_inc
            learned.remove(-pivot_lit)
            for lit in antecedent:
                if lit != pivot_lit:
                    learned.add(lit)

        learned_clause = list(learned)
        for lit in learned_clause:
            self.activity[abs(lit)] += self.var_inc
        self.var_inc /= self.var_decay
        levels = sorted({self.level[abs(lit)] for lit in learned_clause}, reverse=True)
        backjump_level = levels[1] if len(levels) > 1 else 0
        return learned_clause, backjump_level

    def backtrack(self, target_level: int) -> None:
        while self.trail and self.level[abs(self.trail[-1])] > target_level:
            lit = self.trail.pop()
            var = abs(lit)
            del self.assigns[var], self.level[var], self.reason[var]
        self.decision_level = target_level

    def solve(self) -> Tuple[bool, Optional[Dict[int, bool]]]:
        if self.bcp() is not None:
            return False, None
        while True:
            unassigned = [v for v in range(1, self.num_vars + 1) if v not in self.assigns]
            if not unassigned:
                return True, dict(self.assigns)
            branch_var = max(unassigned, key=lambda v: self.activity[v])
            self.decision_level += 1
            self.assign(branch_var, self.decision_level, reason=None)
            while True:
                conflict = self.bcp()
                if conflict is None:
                    break
                if self.decision_level == 0:
                    return False, None
                learned_clause, backjump_level = self.analyze_conflict(conflict)
                self.clauses.append(learned_clause)
                self.backtrack(backjump_level)

7. Física estadística y la transición de fase del \(k\)-SAT aleatorio (\(\alpha_c \approx 4.267\))

¿Por qué los solucionadores CDCL resuelven circuitos industriales con \(10^7\) variables en segundos pero se bloquean ante fórmulas 3-SAT aleatorias de solo \(700\) variables? En una fórmula 3-SAT uniforme con \(n\) variables y \(m = \alpha n\) cláusulas (densidad de cláusulas a variables \(\alpha = m / n\)), el método del primer momento arroja para el número esperado de soluciones \(\mathbb{E}[Z]\):

Mediante el método de la cavidad y la ruptura de simetría de réplicas de un paso (1RSB) de la física de vidrios de espín, Mézard, Parisi y Zecchina (2002) determinaron el umbral crítico exacto del 3-SAT aleatorio:

  flowchart TD
    subgraph PhaseTransition["Transición de fase del 3-SAT aleatorio según la densidad α = m/n"]
        S1["1. Fase líquida sub-restringida (α < 3.86 : Easy-SAT)<br/>• Las soluciones forman un único clúster gigante conectado en {0,1}^n<br/>• Solución rápida en tiempo polinomial"]
        S2["2. Fase vítrea de fragmentación y congelamiento (3.86 < α < 4.267 : Hard-SAT)<br/>• En α_d ≈ 3.86 (transición 1RSB), el espacio de soluciones se fragmenta en exponencialmente muchas islas aisladas!<br/>• En α_f ≈ 4.254 las variables dentro de cada isla quedan rígidamente congeladas (Freezing)"]
        S3["3. Umbral crítico de satisfacibilidad (α_c ≈ 4.267 : Pico máximo de dureza)<br/>• La probabilidad de SAT cae abruptamente de 1 a 0<br/>• Toda refutación por resolución exige longitud exponencial 2^Ω(n) (Chvátal–Szemerédi)"]
        S4["4. Fase sobre-restringida (α > 4.267 : Easy-UNSAT)<br/>• La alta densidad de cláusulas genera contradicciones a poca profundidad<br/>• El tamaño de la prueba disminuye al crecer α"]
    end
    S1 -->|"α_d ≈ 3.86 (Fragmentación)"| S2
    S2 -->|"α_c ≈ 4.267 (Transición UNSAT)"| S3
    S3 -->|"α > 4.267 (Conflictos superficiales)"| S4

En \(\alpha_c \approx 4.267\), el hipergrafo aleatorio es un grafo expansor sin cuellos de botella locales, lo que obliga a cualquier refutación por resolución a tener un tamaño exponencial \(2^{\Omega(n)}\) (Chvátal & Szemerédi, 1988). Por el contrario, los problemas industriales reales diseñados por humanos poseen una rica estructura modular:

1. Modularidad y estructura comunitaria (Ansótegui et al. 2012): los circuitos y programas constan de módulos débilmente acoplados mediante pocas variables de interfaz, que la resolución 1-UIP identifica como dominadores para aprender cláusulas Glue cortas (\(\text{LBD}=2\)).
2. Conjuntos «Backdoor» pequeños (Williams, Gomes, Selman 2003): basta con asignar unas pocas decenas de variables clave \(B \subset V\) (\(|B| \ll n\)) para que el resto de los millones de variables se resuelva íntegramente mediante propagación unitaria BCP.

8. Triunfos en el mundo real y la demostración matemática de 200 Terabytes

1. Matemáticas asistidas por computadora y la prueba DRAT de 200 TB (Heule, Kullmann, Marek 2016): ¿Se puede colorear \(\{1, \dots, N\}\) con dos colores sin que exista ninguna terna pitagórica \(a^2 + b^2 = c^2\) monocromática? Usando Cube-and-Conquer en 800 núcleos, demostraron que \(N = 7824\) es satisfacible (SAT) pero \(N = 7825\) es insatisfacible (UNSAT), generando un certificado formal DRAT de 200 Terabytes verificado bit a bit. Con la misma técnica resolvieron el número de Schur \(S(5) = 160\) (2018) y la conjetura de Keller en dimensión 7 (2020).
2. Verificación formal de chips EDA (CEC y BMC): desde el error FDIV del Pentium de Intel (1994), todo microprocesador se verifica construyendo un circuito Miter (XOR entre especificación RTL y compuertas) resuelto mediante SAT.
3. Gestores de paquetes (Debian apt, Rust Cargo, Dart PubGrub, uv): el algoritmo PubGrub ejecuta CDCL directamente sobre rangos de versiones y traduce el grafo de resolución 1-UIP en mensajes de error legibles para humanos.
4. De SAT a SMT (\(\text{DPLL}(T)\): Z3 y cvc5): acoplando CDCL con solucionadores de teorías (aritmética lineal, vectores de bits, arreglos), los solucionadores SMT impulsan la ejecución simbólica y el motor de seguridad en la nube AWS Zelkova.