DPLL

DPLL ( algoritmo de Davis-Putnam-Logeman-Loveland ) es un algoritmo de retroceso completo para resolver el problema CNF-SAT  : determinar la satisfacibilidad de las fórmulas booleanas escritas en forma normal conjuntiva .

Publicado en 1962 por Martin Davis , Hilary Putnam , George Logeman y Donald Loveland como una mejora del anterior algoritmo de Davis-Putnam basado en la regla de resolución .

Es un algoritmo altamente eficiente y sigue siendo relevante después de medio siglo y se utiliza en la mayoría de los solucionadores de SAT y sistemas de prueba automática para fragmentos de lógica de primer orden [1] .

Implementaciones y aplicaciones

El problema de la satisfacibilidad de las fórmulas booleanas es importante tanto desde el punto de vista teórico como práctico. En la teoría de la complejidad, este es el primer problema para el que se ha demostrado la pertenencia a la clase de problemas NP-completos . También puede aparecer en una amplia variedad de aplicaciones prácticas, como verificación de modelos , programación y diagnóstico.

Esta área fue y sigue siendo un área de investigación en crecimiento, anualmente se realizan competencias entre diferentes solucionadores de SAT [2] ; Las implementaciones modernas del algoritmo DPLL, como Chaff , zChaff [3] [4] , GRASP y Minisat [5] , ocupan el primer lugar en dichas competencias.

Otro tipo de aplicación en la que se suele utilizar DPLL son los sistemas de demostración de teoremas .

Descripción del algoritmo

El algoritmo de retroceso básico comienza seleccionando una variable, estableciéndola en verdadero, simplificando la fórmula y luego probando recursivamente la fórmula simplificada para determinar su factibilidad; si es factible, entonces la fórmula original también es factible; de lo contrario, se repite el procedimiento, pero la variable seleccionada se establece en falso. Este enfoque se denomina "regla de división" porque divide la tarea en dos subtareas más simples. El paso de simplificación consiste en eliminar todas las cláusulas de la fórmula que se vuelven verdaderas después de asignar el valor "verdadero" a la variable seleccionada y eliminar de las cláusulas restantes todas las ocurrencias de esta variable que se vuelven falsas.

El algoritmo DPLL mejora el algoritmo de retroceso básico mediante el uso de las siguientes reglas en cada paso:

Propagación variable si una cláusula contiene exactamente una variable a la que aún no se le ha asignado un valor, esa cláusula solo puede convertirse en verdadera si a la variable se le asigna un valor que la hace verdadera (verdadera si la variable está en la cláusula sin negación, y falsa si la variable es negativo). Por lo tanto, no hay necesidad de hacer una elección en este paso. En la práctica, esto va seguido de una cascada de asignaciones a variables, lo que reduce significativamente el número de opciones de iteración. Exclusión de variables "puras" si alguna variable entra en la fórmula con una sola "polaridad" (es decir, solo sin negaciones o solo con negaciones), se llama pura . A las variables "puras" siempre se les puede dar un valor tal que todas las cláusulas que las contengan se vuelvan verdaderas. Por lo tanto, estas cláusulas no afectarán el espacio de variantes, y pueden eliminarse.

La insatisfacción para valores de variables específicas dados se define cuando una de las cláusulas se vuelve "vacía", es decir, todas sus variables reciben valores de tal manera que sus ocurrencias (con o sin negación) se vuelven falsas. La satisfacibilidad de una fórmula se establece cuando todas las variables se establecen en valores para que no haya cláusulas "vacías" o, en las implementaciones modernas, si todas las cláusulas son verdaderas. La insatisfacción de toda la fórmula sólo puede establecerse después del final de la enumeración exhaustiva.

El algoritmo DPLL se puede expresar usando el siguiente pseudocódigo, donde Φ denota una fórmula en forma normal conjuntiva:

Datos de entrada: un conjunto de cláusulas de la fórmula Φ. Salida: valor de verdad función DPLL(Φ) si Φ es el conjunto de cláusulas ejecutables , devuelve verdadero; si Φ contiene una cláusula vacía , devuelve false; para cada cláusula de una variable l a Φ Φ unidad de propagación ( l , Φ); para cada variable l que ocurre en forma pura en Φ Φ asignación de literal puro ( l , Φ); l elegir-literal (Φ); devuelve DPLL (Φ&l) o DPLL (Φ¬(l));

En este pseudocódigo unit-propagate(l, Φ), y pure-literal-assign(l, Φ) son funciones que devuelven el resultado de aplicar a una variable ly una fórmula de propagación de variable Φy una regla de exclusión de "variable pura", respectivamente. En otras palabras, reemplazan cada ocurrencia de una variable lcon verdadero y cada ocurrencia de una variable negada con not lfalso en la fórmula Φy luego simplifican la fórmula resultante. El pseudocódigo anterior solo devuelve una respuesta: si el último de los conjuntos de valores asignados cumple con la fórmula. En las implementaciones modernas, los conjuntos de ejecución parcial también regresan en caso de éxito.

El algoritmo depende de la elección de una "variable de rama", es decir, una variable que se selecciona en el siguiente paso del algoritmo con un retorno. para asignarle un valor específico. Por lo tanto, no es un algoritmo, sino toda una familia de algoritmos, uno para cada forma posible de elegir "variables de rama". La eficiencia del algoritmo depende en gran medida de esta elección: hay ejemplos de problemas para los que el tiempo de ejecución del algoritmo puede ser constante o crecer exponencialmente, dependiendo de la elección de las "variables de rama". Los métodos de selección son técnicas heurísticas y también se denominan "heurísticas de ramificación" [6] .

Investigación contemporánea

La investigación actual para mejorar el algoritmo se lleva a cabo en tres direcciones: la definición de varios métodos de optimización para elegir una "variable de rama"; desarrollo de nuevas estructuras de datos para acelerar el algoritmo, especialmente para la propagación de variables; y desarrollo de varias variantes del algoritmo básico de backtracking. La última dirección incluye "retroceso no cronológico" y recordar casos malos . Estas mejoras se pueden describir como un método de retorno después de que se llega a una cláusula falsa, en el que se recuerda qué asignación particular de un valor a una variable causó este resultado para evitar exactamente la misma secuencia de cálculos en el futuro, reduciendo así tiempo de trabajo.

Un algoritmo más nuevo, el método Stalmark, se conoce desde 1990. También desde 1986 se han utilizado diagramas de decisión para resolver el problema del SAT.

Basado en el algoritmo DPLL, el algoritmo CDCL se creó a mediados de la década de 1990 y se ha vuelto ampliamente utilizado .

Notas

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), Abstract DPLL and Abstract DPLL Modulo Theories , Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings : 36–50 , < http://www.lsi.upc.edu /~roberto/papers/lpar04.pdf > Archivado el 17 de noviembre de 2011 en Wayback Machine . 
  2. ↑ La página web de los Concursos internacionales del SAT , sat! live , < http://www.satcompetition.org/ > Archivado el 12 de febrero de 2005 en Wayback Machine . 
  3. ↑ Sitio web de zChaff , < http://www.princeton.edu/~chaff/zchaff.html > Archivado el 19 de abril de 2017 en Wayback Machine . 
  4. ↑ Sitio web de Chaff , < http://www.princeton.edu/~chaff/ > Archivado el 23 de febrero de 2020 en Wayback Machine . 
  5. ↑ Sitio web de Minisat . Archivado desde el original el 20 de abril de 2012.
  6. ↑ Marqués-silva, Joao. El impacto de las heurísticas de ramificación en los algoritmos de satisfacibilidad proposicional  (inglés)  // En la 9ª Conferencia Portuguesa de Inteligencia Artificial (EPIA): revista. - 1999. - doi : 10.1.1.111.9184 . Archivado desde el original el 14 de abril de 2012.

Literatura