Un mecanismo de resolución SAT que analiza los conflictos encontrados durante la búsqueda para derivar y registrar nuevas cláusulas (cláusulas aprendidas) que evitan que el mismo patrón de conflicto ocurra en ramas posteriores de la búsqueda, típicamente combinado con retroceso no cronológico.

Principio

Cuando se detecta un conflicto, construir un grafo de implicación a partir de las asignaciones recientes, identificar un corte o Punto de Implicación Único (UIP), derivar una cláusula que bloquee el conflicto (una consecuencia lógica del conjunto de cláusulas), añadirla a la base y retroceder al nivel de decisión correspondiente.

Demostración

Durante la búsqueda, la propagación unitaria conduce a un conflicto de cláusulas. Construir el grafo de implicación de los literales asignados, encontrar el primer UIP, resolver cláusulas a lo largo del corte para generar una cláusula aprendida ¬a ∨ ¬b que impide repetir la misma combinación conflictiva, y luego retroceder al nivel de decisión donde esa cláusula se vuelve unitaria.

Aplicación incorrecta

Registrar cláusulas que no son consecuencias lógicas (derivación incorrecta), aprender cláusulas excesivamente específicas o trivialmente subsumidas sin política de eliminación, o tratar las cláusulas aprendidas como meras heurísticas sin garantizar la corrección socava la exactitud o el rendimiento del solver.

Consecuencia

CDCL evita la exploración repetida de los mismos patrones de conflicto, permite un retroceso no cronológico potente y es una razón principal de las aceleraciones prácticas drásticas que obtienen los solve r SAT modernos en muchas clases de problemas.

Inversión

DPLL puro sin aprendizaje de cláusulas redescubre repetidamente los mismos conflictos y suele ser mucho menos eficiente; los métodos de búsqueda local también evitan el aprendizaje y presentan un perfil de rendimiento distinto.

Límite

Se aplica a la resolución proposicional basada en cláusulas y a extensiones con razonamiento teórico cuando están cuidadosamente integradas; requiere análisis de conflicto correcto y gestión de la base de cláusulas aprendidas (recogida de basura, subsunción) para ser eficaz.

Tensión semántica

CDCL equilibra entre aprender demasiadas cláusulas (explosión de memoria/tiempo) y aprender muy pocas (poda ineficaz); se sitúa entre los sistemas de prueba basados en resolución pura y la búsqueda heurística, mezclando deducción con control de búsqueda.

Síntesis

El aprendizaje de cláusulas dirigido por conflictos es el proceso de analizar conflictos mediante grafos de implicación para extraer cláusulas aprendidas válidas y realizar retrocesos dirigidos, produciendo una base dinámica de cláusulas que poda la búsqueda futura y potencia la resolución SAT moderna.