Aprendizaje de cláusulas basado en conflictos

Algoritmo de resolución SAT

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

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

Fondo

Problema de satisfacibilidad booleana

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

Un ejemplo de tal fórmula es:

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

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

${\displaystyle (\lnot A\lor \lnot C)\land (B\lor C)}$

donde A , B , C son variables booleanas, , , y son literales y y son cláusulas. ${\displaystyle \lnot A}$ ${\displaystyle \lnot C}$ ${\displaystyle B}$ ${\displaystyle C}$ ${\displaystyle \lnot A\lor \lnot C}$ ${\displaystyle B\lor C}$

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

${\displaystyle A=\mathrm {False} ,B=\mathrm {False} ,C=\mathrm {True} }$

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

Este ejemplo utiliza tres variables ( A , B , C ) y hay dos asignaciones posibles (Verdadero y Falso) para cada una de ellas. Entonces 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 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 tarea satisfactoria de manera eficiente y rápida aplicando diferentes heurísticas para fórmulas CNF complejas. ${\displaystyle 2^{3}=8}$

Regla de la cláusula unitaria (propagación unitaria)

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

La aplicación iterada de la regla de la cláusula unitaria se conoce como propagación unitaria o propagación de restricciones booleanas (BCP).

Resolución

Considere dos cláusulas y . La cláusula , obtenida fusionando las dos cláusulas y eliminando ambas y , se llama resolutiva 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)}$ ${\displaystyle \neg C}$ ${\displaystyle C}$

Algoritmo

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

1. Seleccione una variable y asígnele Verdadero o Falso. A esto se le llama estado de decisión. Recuerda la tarea.
2. Aplicar propagación de restricciones booleanas (propagación unitaria).
3. Construya el gráfico de implicaciones .
4. Si hay algún conflicto
   1. Encuentre el corte en el gráfico de implicaciones que llevó al conflicto.
   2. Derivar una nueva cláusula que sea la negación de las cesiones que dieron lugar al conflicto.
   3. Retroceder de forma no cronológica ("salto 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.

Ejemplo

Un ejemplo visual del algoritmo CDCL: ^[4]

• 
  Primero elija una variable de ramificación, concretamente 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 de la unidad. El gráfico resultante se llama gráfico de implicaciones .
• 
  Elija arbitrariamente otra variable de ramificación, x3 .
• 
  Aplique la propagación unitaria y encuentre el nuevo gráfico de implicaciones.
• 
  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!
• 
  Encuentra el corte que llevó a este conflicto. Del corte, encuentre una condición conflictiva.
• 
  Tome la negación de esta condición y conviértala en una cláusula.
• 
  Agregue 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 en consecuencia.

Lo completo

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 la solidez ni la integridad. El análisis de conflictos identifica nuevas cláusulas mediante la operación de resolución. Por lo tanto, cada cláusula aprendida se puede inferir de las cláusulas originales y de otras cláusulas aprendidas mediante una secuencia de pasos de resolución. Si cN es la nueva cláusula aprendida, entonces ϕ es satisfactoria si y sólo si ϕ ∪ {cN} también es satisfactoria. Además, el paso de retroceso modificado tampoco afecta la solidez o integridad, ya que la información de retroceso se obtiene de cada nueva cláusula aprendida. ^[5]

Aplicaciones

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

• MiniSAT
• 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 áreas de aplicaciones 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.

Algoritmos relacionados

Los algoritmos relacionados con CDCL son el algoritmo de Davis-Putnam y el algoritmo DPLL . El algoritmo DP utiliza refutación de resolución y tiene posibles problemas de acceso a la memoria. ^{[ cita necesaria ]} Mientras que el algoritmo DPLL está bien para instancias generadas aleatoriamente, es malo para instancias generadas en aplicaciones prácticas. CDCL es un enfoque más poderoso para resolver estos problemas porque la aplicación de CDCL proporciona menos 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.

Trabajos citados

1. JP Marques-Silva; Karem A. Sakallah (noviembre de 1996). "GRASP-Un nuevo algoritmo de búsqueda de satisfacción". Resumen de la Conferencia Internacional IEEE sobre Diseño Asistido por Computadora (ICCAD) . págs. 220–227. CiteSeerX  10.1.1.49.2075 . doi :10.1109/ICCAD.1996.569607. ISBN 978-0-8186-7597-3.
2. JP Marques-Silva; Karem A. Sakallah (mayo de 1999). "GRASP: un algoritmo de búsqueda para la satisfacibilidad proposicional" (PDF) . Transacciones IEEE en computadoras . 48 (5): 506–521. doi : 10.1109/12.769433. Archivado desde el original (PDF) el 4 de marzo de 2016 . Consultado el 29 de noviembre de 2014 .
3. Roberto J. Bayardo Jr.; Robert C. Schrag (1997). "Uso de técnicas retrospectivas de CSP para resolver instancias SAT del mundo real" (PDF) . Proc. 14° Nacional. Conf. sobre Inteligencia Artificial (AAAI) . págs. 203–208.
4. En las imágenes a continuación, " " se usa para denotar "o", la multiplicación para denotar "y" y un sufijo " " para denotar "no". ${\displaystyle +}$ ${\displaystyle '}$
5. Biere, Heule, Van Maaren, Walsh (febrero de 2009). Manual de satisfacibilidad (PDF) . Prensa IOS. pag. 138.ISBN​ 978-1-60750-376-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
6. "Página de inicio de glucosa".

Referencias

• Martín Davis; Hilary Putnam (1960). "Un procedimiento de cálculo para la teoría de la cuantificación". J. ACM . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376.
• Martín 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.
• Mateo W. Moskewicz; Conor F. Madigan; Ying Zhao; Lintao Zhang; Sharad Malik (2001). "Chaff: ingeniería de un solucionador SAT eficiente" (PDF) . Proc. 38º Ana. Conferencia de automatización de diseño (DAC) . págs. 530–535.
• Lintao Zhang; Conor F. Madigan; Mateo H. Moskewicz; Sharad Malik (2001). "Aprendizaje eficiente impulsado por conflictos en un solucionador de satisfacibilidad booleano" (PDF) . Proc. IEEE/ACM Int. Conf. sobre Diseño asistido por ordenador (ICCAD) . págs. 279–285.
• Presentación – "SAT-Solving: De Davis-Putnam a Zchaff y más allá" por Lintao Zhang. (Varias fotografías son tomadas de su presentación)