##  [Aprendizaje de Cláusulas Dirigido por Conflictos (CDCL)](/es/node/60849) 

 Definición

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

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

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

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

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

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

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

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

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.