[MÚSICA] Hola, soy Stalin Muñoz y les voy a hablar del algoritmo DPLL para resolver el problema de satisfactibilidad booleana. Este algoritmo se denomina DPLL en honor a los investigadores Davies, Putnam, Logemann y Loveland. Como la mayoría de los algoritmos recursivos, DPLL descompone un problema complejo en subproblemas más simples. La estrategia de los algoritmos de búsqueda con retroceso es la siguiente. Se comienza por asignar una solución parcial. De manera sistemática e incremental, se busca una solución completa. Si en algún momento el algoritmo determina que no va a conducir a una solución completa, retrocede y asigna otra solución parcial. Estos pasos se repiten hasta determinar la solución completa o que no exista solución al problema. El objetivo del algoritmo es simplificar la fórmula hasta determinar el valor cierto, es decir, que la fórmula es satisfactible. En este ejemplo, tenemos la cláusula A disyunción B. Para simplificarla, asumimos que alguna de las variables toma un valor de verdad particular. Por ejemplo, si A es cierta, concluimos inmediatamente que la fórmula es satisfactible. Si por el contrario consideramos que A es falsa, entonces la fórmula se simplifica a la cláusula B. A su vez, esta cláusula puede simplificarse asumiendo algún valor para B. Si elegimos el valor cierto, entonces concluimos cierto. Si elegimos el valor falso, concluimos falso. En el caso de encontrar alguna fórmula falsa, el algoritmo debe continuar buscando. Para determinar satisfactibilidad, es necesario encontrar un valor cierto. Vamos a definir la simplificación de una cláusula en forma normal conjuntiva con una literal. Imaginemos que tenemos la fórmula con el conjunto de cláusulas y esta literal aparece en alguna de ellas. En esa cláusula, como está en forma afirmada, vamos a eliminar la cláusula completamente al simplificarla porque esta se vuelve verdadera y está en conjunción con las otras cláusulas. Mientras que si aparece en su forma complementaria, es decir, en su forma negada de la literal, entonces eliminamos la literal, porque esta se vuelve falsa y está en disyunción con las otras literales. En este ejemplo, la fórmula fi tiene dos cláusulas. Vamos a simplificar la fórmula con la literal B. La primera cláusula se elimina porque la literal B aparece con el mismo signo. La segunda cláusula tiene la literal complementaria, entonces borramos dicha literal. El resultado es una fórmula con una sola cláusula. Los casos base del algoritmo DPLL son aquellos que se pueden resolver de manera trivial. Hay dos casos. Uno, cuando la fórmula se vuelve falsa. Esto es a través de que las cláusulas, o alguna de ellas, se volvieron falsas, es decir, no tienen literales. El otro caso es cuando you no hay cláusulas, porque todas ellas se volvieron verdaderas y se eliminaron de la fórmula. Otro concepto importante para el algoritmo es el de cláusula unitaria. Una cláusula unitaria es aquella que contiene solo una literal. Y también es importante el concepto de literal pura. Una literal pura es aquella que aparece con el mismo signo en todas las cláusulas. Por ejemplo, en la fórmula siguiente A es pura, pero tanto B como C no lo son. Si la fórmula original es satisfactible al simplificarla con la literal pura, la fórmula resultante también es satisfactible. A continuación, vamos a ver el algoritmo DPLL. La entrada del algoritmo DPLL es la fórmula en forma normal conjuntiva. La salida es verdadero cuando la fórmula es satisfactible y falso cuando no lo es. Los primeros dos pasos, el uno y el dos, se refieren a los casos base. En el primero, si la expresión es vacía, significa que todas las cláusulas se lograron, es decir, que la fórmula es satisfactible. Y el caso dos es el caso de la contradicción, o sea que la cláusula no se puede lograr o no se puede hacer verdadera. En el paso tres, tenemos la cláusula unitaria. Si existe una cláusula unitaria, simplificamos con la literal que aparece en esa cláusula unitaria e invocamos el algoritmo de manera recursiva. En el paso cuatro tenemos una literal pura, entonces asumimos esa literal simplificando la cláusula original. En el paso cinco, seleccionamos una variable de manera arbitraria. En el paso seis, simplificamos la fórmula con la literal donde la variable seleccionada está afirmada e invocamos de manera recursiva el algoritmo DPLL. Si el algoritmo nos regresa cierto, concluimos satisfactibilidad. Pero si nos regresa falso, entonces vamos al paso siete. En el paso siete, vamos a probar con la literal complementaria. Simplificamos la fórmula e invocamos de manera recursiva al algoritmo DPLL. El resultado de esta invocación es lo que regresará el algoritmo. Para ejemplificar la aplicación del algoritmo DPLL, vamos a retomar el ejemplo del homicidio en el tren. Aquí tenemos la víctima, el detective y dos sospechosos del homicidio. Vamos a definir variables booleanas para este problema. DA representa, el detective está en el vagón A. S1A representa, el sospechoso 1 está en el vagón A. CS1 representa, el sospechoso 1 tiene cuchillo. SS1 representa, el sospechoso 1 tiene sangre en su pañuelo. S2A, CS2, SS2 representan las mismas proposiciones pero para el sospechoso 2. VA representa, la víctima está en el vagón A. S1MV significa que el sospechoso 1 mata a la víctima. S2MV significa que el asesino es el sospechoso 2. Tenemos ciertas pistas. Sabemos que alguno de los sospechosos mató a la víctima. Esto lo representamos con la disyunción de S1MV y S2MV. Sabemos que si el sospechoso 1 mató a la víctima, entonces tiene un cuchillo y sangre en su pañuelo, además de que tanto el sospechoso como la víctima están en el mismo vagón pero el detective en otro. Sabemos lo mismo para el sospechoso 2. Finalmente, sabemos que no todos estuvieron en el vagón A. Para aplicar DPLL, transformamos las fórmulas a forma normal conjuntiva. Quitamos la implicación con su forma equivalente. En la fórmula que representa la consecuencia de la implicación, distribuimos para que nos quede la disyunción de literales. Distribuimos nuevamente, logrando la forma deseada. Aquí ponemos en conjunción todas las fórmulas, resultando una fórmula con 18 cláusulas. Vamos a alimentar la fórmula a DPLL y vemos qué pasa. Vemos que la fórmula no es vacía, no hay cláusulas sin literales, no hay cláusulas unitarias, pero existe una literal pura, SS1. DPLL simplifica la fórmula, regresará el resultado de la invocación recursiva con la fórmula simplificada. DPLL, operando la fórmula simplificada, determina que existe la literal pura CS1. Simplifica la fórmula, regresará el resultado de la invocación con la fórmula simplificada. Continuamos. Literal pura SS2, simplificación. Literal pura CS2, simplificación. Elige una variable arbitraria S1A. Este es un punto de posible bifurcación. El algoritmo regresará este punto en caso de que la simplificación no nos conduzca a cierto. Literal de A, cláusula unitaria negado de S1MV. Cláusula unitaria negado de S2MV. Caso base, cláusula sin literales. El algoritmo retrocede al punto de posible bifurcación. Asignamos la literal complementaria en este punto, negado de VA. Simplificamos literal VA, simplificamos literal pura S1MV, simplificamos literal pura S2A, simplificamos caso base, fórmula sin cláusulas. Concluimos que la fórmula es satisfactible. [MÚSICA] [MÚSICA] [MÚSICA]
