El algoritmo CDCL ( conflict-driven clausula learning ) es un solucionador eficiente ( NP-completo ) de problemas de satisfacibilidad para fórmulas booleanas (SAT solver) basado en el algoritmo DPLL . La principal estructura de datos en los solucionadores de CDCL es un gráfico de implicación que captura las asignaciones a las variables, y otra característica es el uso de cláusulas de recuerdo y retroceso no cronológico durante el análisis de conflictos.
El algoritmo fue propuesto por João Marques -Silva y Karem A. Sakallah en 1996 [ 1] e independientemente por Roberto J. Bayardo y Robert Schrag ( Robert C. Schrag ) en 1997 [2] [3] .
El algoritmo DPLL que subyace al algoritmo CDCL utiliza backtracking en formas normales conjuntivas , en cada paso del cual se selecciona una variable y se le asigna un valor (0 o 1) para la ramificación posterior, que consiste en asignar un valor a una variable, después de lo cual se simplifica La fórmula se prueba recursivamente para determinar su viabilidad. En el caso de que se encuentre un conflicto , es decir, la fórmula resultante no sea factible, se activa el mecanismo de devolución (backtracking), en el que se cancelan las ramas en las que se intentaron ambos valores para la variable. Si la búsqueda vuelve a una rama de primer nivel, toda la fórmula se declara insatisfactoria . Tal retorno, inherente al algoritmo DPLL, se denomina cronológico [3] .
Los disjuntos utilizados en el algoritmo se dividen en satisfecho (satisfecho), cuando hay 1 entre los valores incluidos en el disyuntivo, insatisfecho (no satisfecho): todos los valores son cero, solo (unidad), todos ceros, excepto uno variable a la que aún no se le ha asignado un valor y sin resolver , todo lo demás. Uno de los componentes más importantes de los solucionadores de SAT es la regla de la disyunción única , en la que la elección de una variable y su valor no son ambiguos. (Cabe recordar que la disyunción incluye tanto las variables como sus negaciones ) . El procedimiento de propagación de unidades ( en los solucionadores de CDCL modernos casi siempre se basa en la regla de la disyunción única) se realiza después de la bifurcación para calcular las consecuencias lógicas de la elección realizada [ 3] .
Además de DPLL y su mecanismo de retroceso, CDCL utiliza otros trucos [3] :
Varios valores auxiliares están asociados con cada variable que se comprueba para la viabilidad de la fórmula en el algoritmo CDCL [3] :
Esquemáticamente, un algoritmo CDCL típico se puede representar de la siguiente manera [3] :
Algoritmo CDCL(φ, ν) aporte: φ - fórmula (CNF) ν - visualización de valores de variables en forma de un conjunto de pares salida: SAT (fórmula satisfactoria) o UNSAT (no satisfactoria) si Conflicto de Propagación de Unidades (φ, ν) después retorno UNSAT L := 0 -- nivel de solución while NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- toma de decisiones L := L + 1 v := v ∪ {(x, v)} si UnitPropagationConflict(φ, ν) -- consecuencias de salida después β := ConflictAnalysis(φ, ν) -- diagnóstico de conflicto si β < 0 después retorno UNSAT de lo contrario Retroceder (φ, ν, β) -- volver (retroceder) L := β sáb regresoEste algoritmo utiliza varias subrutinas que, además de devolver valores, también pueden cambiar las variables φ, ν [3] que se les pasan por referencia :
El procedimiento de análisis de conflictos es fundamental para el algoritmo CDCL.
La principal estructura de datos utilizada en los solucionadores de CDCL es un gráfico de implicación que fija asignaciones a variables (tanto como resultado de decisiones como aplicando la regla de disyunción única), en el que los vértices corresponden a fórmulas literales y los arcos fijan la estructura de implicaciones [ 4 ] [5] .
El procedimiento de análisis de conflictos (ver el diagrama del algoritmo) se llama cuando se detecta un conflicto de acuerdo con la regla de cláusula única, y sobre esta base se repone el conjunto de cláusulas memorizadas. El procedimiento comienza en el nodo del gráfico de implicación donde se encuentra el conflicto, y recorre los niveles de decisión con números más bajos, retrocediendo por las implicaciones hasta encontrar la variable asignada más recientemente (como resultado de la decisión) [3] . Las cláusulas memorizadas se utilizan en el retroceso no cronológico , que es otra técnica típica de los solucionadores de CDCL [6] .
Para comparacion:
DPLL : sin memorización de cláusulas, retorno cronológico.
CDCL: memorización de cláusulas como resultado del análisis de conflictos y backtracking no cronológico
La idea de utilizar la estructura de implicaciones que condujo al conflicto se desarrolló hacia el uso de UIP ( Ing. Unit Implication Points - "puntos de implicación únicos"). UIP es el dominador de gráfico de implicación , que se puede calcular en tiempo lineal para este tipo de gráfico. La UIP es una asignación de variable alternativa, y se garantiza que la cláusula almacenada en el primer punto de este tipo tendrá el tamaño más pequeño y proporcionará la mayor reducción en el nivel de solución. Debido al uso de estructuras de datos perezosas eficientes, los autores de muchos solucionadores de SAT, por ejemplo, Chaff, utilizan el primer método UIP para memorizar cláusulas ( aprendizaje de la primera cláusula UIP ) [3] .
Al igual que DPLL , el algoritmo CDCL es un solucionador de SAT correcto y completo. Así, la memorización de cláusulas no afecta a la exhaustividad y corrección, ya que cada cláusula memorizada puede deducirse de las cláusulas iniciales y de otras cláusulas memorizadas por el método de resolución . El mecanismo de devolución modificado tampoco afecta la integridad y corrección, ya que la información sobre la devolución se almacena en la cláusula memorizada [3] .
Ilustración de la operación del algoritmo:
Selección de variable de rama: x1 . El círculo amarillo significa una decisión arbitraria.
De acuerdo con la regla de la cláusula singular , x4 debe ser 1. El círculo gris es una asignación forzada. El gráfico resultante es el gráfico de implicación.
Una elección arbitraria de otra variable, x3 .
Aplicación de la regla de la cláusula unitaria y búsqueda de un nuevo gráfico de implicación.
Las variables x8 y x12 toman lógicamente los valores 0 y 1, respectivamente.
Selección de variable de bifurcación nuevamente: x2 .
Construcción de un gráfico de implicación.
Otra variable: x7 .
Construcción de un gráfico de implicación.
Nuevo gráfico de implicación. Recibido un conflicto .
Encontrar el corte del gráfico que dio lugar al conflicto y la cláusula de conflicto.
Encontrar una disyunción por negación: si de a sigue b , entonces de no-b sigue no-a
Recordando la disyunción.
Retorno no cronológico al nivel de decisión apropiado.
Valores de ajuste apropiados.
Los solucionadores de SAT basados en el algoritmo CDCL encuentran aplicación en la demostración automática de teoremas , criptografía , verificación de modelos y pruebas de hardware y software, bioinformática , determinación de dependencias en sistemas de gestión de paquetes , etc. [3]