Aprendizaje de cláusulas basado en conflictos

En informática , el aprendizaje de cláusulas impulsado por 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 toda la fórmula evalúe como verdadera. El funcionamiento interno de los solucionadores SAT de CDCL se inspiró en los solucionadores DPLL . La principal diferencia entre CDCL y DPLL es que el salto hacia atrás de CDCL no es cronológico.

Marques-Silva y Karem A. Sakallah (1996, 1999) ^{[1] [2]} y Bayardo y Schrag (1997) propusieron el aprendizaje de cláusulas impulsado por conflictos . ^[3]

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

Un ejemplo de dicha fórmula es:

( ( no A ) o ( no C ) )   y   ( B o C ),

o, utilizando una notación común: ^[4]

${\displaystyle (\lno A\lo \lno C)\land (B\lo C)}$

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

Una tarea satisfactoria para esta fórmula es, por ejemplo:

${\displaystyle A=\mathrm {Falso}, B=\mathrm {Falso}, C=\mathrm {Verdadero}}$

ya que hace que la primera cláusula sea verdadera (ya que es verdadera) así como también la segunda (ya que es verdadera). ${\displaystyle \lno A}$${\estilo de visualización C}$

Este ejemplo utiliza tres variables ( A , B , C ) y hay dos asignaciones posibles (Verdadero y Falso) para cada una de ellas. Por lo tanto, hay posibilidades. En este pequeño ejemplo, se puede utilizar la búsqueda por fuerza bruta para probar todas las asignaciones posibles y comprobar si satisfacen 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 asignación satisfactoria de manera eficiente y rápida aplicando diferentes heurísticas para fórmulas CNF complejas. ${\displaystyle 2^{3}=8}$

Si una cláusula tiene todos sus literales o variables menos uno evaluados como Falso, entonces el literal libre debe ser Verdadero para que la cláusula sea Verdadera. Por ejemplo, si la cláusula insatisfecha a continuación se evalúa con y debemos tener para que la cláusula sea verdadera. ${\displaystyle A=\mathrm {Falso} }$${\displaystyle B=\mathrm {Falso} }$${\displaystyle C=\mathrm {Verdadero} }$${\displaystyle (A\lor B\lor C)}$

La aplicación iterada de la regla de la cláusula de unidad se denomina propagación de unidad o propagación de restricción booleana (BCP).

Consideremos dos cláusulas y . La cláusula , obtenida al fusionar las dos cláusulas y eliminar tanto y , se denomina resolutor de las dos cláusulas. ${\displaystyle (A\lor B\lor C)}$${\displaystyle (\neg C\lor D\lor \neg E)}$${\displaystyle (A\lor B\lor D\lor \neg E)}$${\estilo de visualización \neg C}$${\estilo de visualización C}$

El aprendizaje de cláusulas basado en conflictos funciona de la siguiente manera.

1. Seleccione una variable y asígnele Verdadero o Falso. Esto se llama estado de decisión. Recuerde la asignación.
2. Aplicar propagación de restricciones booleanas (propagación unitaria).
3. Construye el gráfico de implicaciones .
4. Si hay algún conflicto
   1. Encuentra el corte en el gráfico de implicaciones que llevó al conflicto.
   2. Deriva una nueva cláusula que sea la negación de las cesiones que dieron lugar al conflicto.
   3. Retroceder de forma no cronológica ("saltar hacia atrás") hasta el nivel de decisión apropiado, donde se asignó la primera variable asignada involucrada en el conflicto
5. De lo contrario, continúe desde el paso 1 hasta que se asignen todos los valores de las variables.

Un ejemplo visual del algoritmo CDCL: ^[4]

• 
  En primer lugar, elija una variable de ramificación, es decir, x1 . Un círculo amarillo significa una decisión arbitraria.
• 
  Ahora aplique la propagación unitaria, lo que da como resultado que x4 debe ser 1 (es decir, verdadero). Un círculo gris significa una asignación de variable forzada durante la propagación unitaria. El gráfico resultante se denomina gráfico de implicación .
• 
  Elija arbitrariamente otra variable de ramificación, x3 .
• 
  Aplique la propagación unitaria y encuentre el nuevo gráfico de implicación.
• 
  Aquí las variables x8 y x12 se fuerzan a ser 0 y 1, respectivamente.
• 
  Elija otra variable de ramificación, x2 .
• 
  Encuentra el gráfico de implicaciones.
• 
  Elija otra variable de ramificación, x7 .
• 
  Encuentra el gráfico de implicaciones.
• 
  ¡Encontré un conflicto!
• 
  Encuentre el corte que provocó este conflicto. A partir del corte, encuentre una condición conflictiva.
• 
  Tome la negación de esta condición y conviértala en una cláusula.
• 
  Añade la cláusula de conflicto al problema.
• 
  Salto hacia atrás no cronológico al nivel de decisión apropiado, que en este caso es el segundo nivel de decisión más alto de los literales en la cláusula aprendida.
• 
  Salte hacia atrás y establezca los valores de las variables según corresponda.

DPLL es un algoritmo sólido y completo para SAT. Los solucionadores CDCL SAT implementan DPLL, pero pueden aprender nuevas cláusulas y retroceder de forma no cronológica. El aprendizaje de cláusulas con análisis de conflictos no afecta ni a la solidez ni a la completitud. El análisis de conflictos identifica nuevas cláusulas utilizando la operación de resolución. Por lo tanto, cada cláusula aprendida se puede inferir de las cláusulas originales y otras cláusulas aprendidas mediante una secuencia de pasos de resolución. Si cN es la nueva cláusula aprendida, entonces ϕ es satisfacible si y solo si ϕ ∪ {cN} también es satisfacible. Además, el paso de retroceso modificado tampoco afecta a la solidez ni a la completitud, ya que la información de retroceso se obtiene de cada nueva cláusula aprendida. ^[5]

La principal aplicación del algoritmo CDCL se encuentra en diferentes solucionadores SAT, incluidos:

• Mini SAT
• Zchaff SAT
• Z3
• Glucosa ^[6]
• MuchosSAT etc.

El algoritmo CDCL ha hecho que los solucionadores SAT sean tan poderosos que se están utilizando de manera efectiva en varias ^{[ cita requerida ]} áreas de aplicación del mundo real como planificación de IA, bioinformática, generación de patrones de prueba de software, dependencias de paquetes de software, verificación de modelos de hardware y software, y criptografía.

Los algoritmos relacionados con CDCL son el algoritmo Davis-Putnam y el algoritmo DPLL . El algoritmo DP utiliza refutación de resolución y tiene un potencial problema de acceso a la memoria. ^{[ cita requerida ]} Mientras que el algoritmo DPLL es adecuado para instancias generadas aleatoriamente, es malo para instancias generadas en aplicaciones prácticas. CDCL es un enfoque más poderoso para resolver tales problemas, ya que la aplicación de CDCL proporciona una menor búsqueda en el espacio de estados en comparación con DPLL.

• 
  DPLL: sin aprendizaje y retroceso cronológico.
• 
  CDCL: aprendizaje de cláusulas basado en conflictos y retroceso no cronológico.

• Martin Davis; Hilary Putnam (1960). "Un procedimiento computacional para la teoría de la cuantificación". J. ACM . 7 (3): 201– 215. doi : 10.1145/321033.321034 . S2CID  31888376.
• Martin Davis; George Logemann; Donald Loveland (julio de 1962). "Un programa de máquina para la demostración de teoremas". Comunicaciones de la ACM . 5 (7): 394– 397. doi :10.1145/368273.368557. hdl : 2027/mdp.39015095248095 . S2CID  15866917.
• Matthew W. Moskewicz; Conor F. Madigan; Ying Zhao; Lintao Zhang; Sharad Malik (2001). "Chaff: ingeniería de un solucionador SAT eficiente" (PDF) . Actas de la 38.ª Conferencia Anual de Automatización del Diseño (DAC) . págs.  530– 535.
• Lintao Zhang; Conor F. Madigan; Matthew H. Moskewicz; Sharad Malik (2001). "Aprendizaje eficiente basado en conflictos en un solucionador de satisfacibilidad booleana" (PDF) . Proc. Conferencia internacional IEEE/ACM sobre diseño asistido por computadora (ICCAD) . págs.  279– 285.
• Presentación: "Resolución de problemas SAT: de Davis-Putnam a Zchaff y más allá", a cargo de Lintao Zhang. (Varias fotografías son de su presentación)