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.