Aprendizaje de cláusulas basado en conflictos

---

En informática , el aprendizaje de cláusulas basado en conflictos ( CDCL ) es un algoritmo para resolver el problema de satisfacibilidad booleano (SAT). Dada una fórmula booleana, el problema SAT solicita una asignación de variables para que la fórmula completa se evalúe como verdadera. El funcionamiento interno de los solucionadores CDCL SAT se inspiró en los solucionadores DPLL .

El aprendizaje de cláusulas basado en conflictos fue propuesto por Marques-Silva y Sakallah (1996, 1999) ^{[1] [2]} y Bayardo y Schrag (1997). ^[3]

El problema de satisfacibilidad consiste en encontrar una asignación satisfactoria para una fórmula dada en forma normal conjuntiva (CNF).

donde A , B , C son variables booleanas, , , y son literales y y son cláusulas.${\ estilo de visualización A'}$${\displaystyle C'}$${\displaystyle B}$${\displaystyle C}$${\displaystyle A'\lor C'}$${\displaystyle B\lor C}$

ya que hace que la primera cláusula sea verdadera (ya que es verdadera) así como la segunda (ya que es verdadera).${\displaystyle A'}$${\displaystyle C}$

Este ejemplo utiliza tres variables ( A , B , C ) y hay dos asignaciones posibles (Verdadero y Falso) para cada una de ellas. Así que uno tiene posibilidades. En este pequeño ejemplo, se puede utilizar la búsqueda de fuerza bruta para probar todas las asignaciones posibles y comprobar si cumplen la fórmula. Pero en aplicaciones realistas con millones de variables y cláusulas, la búsqueda por fuerza bruta no es práctica. La responsabilidad de un solucionador SAT es encontrar una tarea satisfactoria de manera eficiente y rápida mediante la aplicación de diferentes heurísticas para fórmulas CNF complejas.${\displaystyle 2^{3}=8}$

---