Commit 15a0d165 by Stalin Munoz

Initial commit curso IA coursera

parents
Algoritmo DPLL figura de asignación
Las flechas estan muy lejos
agregar paréntesis
------------------------------
5. Algoritmo DPP.
A continuación veremos un algoritmo para solucionar el problema de
satisfactibilidad booleana. El algoritmo DPLL, así nombrado por
corresponder con las iniciales de los apellidos de sus autores:
Davis, Putnam, Logemann y Loveland.
DPLL es un algoritmo recursivo de búsqueda con retroceso.
Como la mayoría de los algoritmos recursivos, la idea es descomponer
un problema complejo en problemas más simples, hasta que
la solución de los subproblemas es trivial.
La estrategia de los algoritmos de búsqueda con retroceso es la siguiente:
Se asigna parcialmente una solución.
Se cominza un procedimiento de construcción sistematica de una solución
completa, mientras la solución candidata sea prometedora.
Si en algún momento el algoritmo determina que la solución candidata
no conducirá a una solución completa, esta se desecha.
El algoritmo retrocede y reasigna otra posible solución parcial candidata.
Estos pasos se repiten hasta encontrar la solución completa o
determinar que no existe solución al problema.
----------------------------------
El objetivo del algoritmo es simplificar la fórmula hasta concluir
el valor de verdad cierto, es decir, que la formula 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.
--------------------------------------------------------
Vamos a definir la simplificación de una formula con una literal l
de la forma siguiete:
Toda cláusula que contenga la literal l se elimina de la formula porque
se simplifica a cierto.
En las cláusulas que contengan la literal complementaria, es decir, la
literal con signo contrario a l, borramos la literal porque se torna falsa.
En este ejemplo la fórmula phi 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 resulado es una fórmula con una sóla cláusula.
------------------------------------------------------------
Los casos base para DPLL, son los casos que se pueden resolver de manera
trivial.
Si eliminamos todas las cláusulas, DPLL determina que la fórmula es
satisfactible porque todas las cláusulas se tornaron ciertas a través de una
serie de asignaciones parciales.
Si DPLL se encuentra con una cláusula sin literales, significa que
la cláusula es falsa y que también la fórmula será falsa pues esta en forma
normal conjuntiva.
--------------------------------------------------------------
Cláusulas con una sola literal se denominan unitarias.
Como el objetivo es concluir cierto, estas se simplifican con la literal que contienen.
En una fórmula que contiene una literal, pero no su literal complementaria,
la literal se denomina pura.
DPLL simplifica la fórmula con la literal pura porque si existe una
asignación que hace la fórmula verdadera, entonces existe una
asignación donde la literal pura es verdadera.
--------------------------------------------------------------
Aquí tenemos el algoritmo.
La entrada es una fórmula en forma normal conjuntiva.
La salida es cierto cuando la formula de entrada es satisfactible,
falso de lo contrario.
Empezamos con los casos base:
Formula vacía, la fórmula es satisfactible.
Existe cláusula vacía, la fórmula es falsa.
Si existe una cláusula unitaria, invocamos recursivamente con la fórmula
simplificada con la literal de la cláusula unitaria.
Si existe una literal pura, invocamos recursivamente con la fórmula
simplificadad con la literal pura.
En otro caso, elegimos cualquier variable v de la fórmula
Si al simplificarla con la literal formada por v la fórmula resultante es
verdadera concluimos satisfactibilidad
En caso contrario, probamos con la literal negada, regresando el resultado
de la invocación recursiva.
----------------------------------
En nuestro ejemplo del tren. Pensemos que hay dos sospechosos del asesinato,
la víctima y el detective del tren.
Definamos variables Booleanas para las siguientes proposiciones:
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 mato 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 estubieron en el vagón A.
--------------------------------------
Para aplicar DPLL lo primero que hacemos es transformar estas fórmulas a
forma normal conjuntiva.
Quitamos la implicación con su forma equivalente.
En la subformula que representaba la consecuencia de la implicación
distribuimos para que nos quede la disyunción de literales.
Distribuimos nuevamente, logrando la fórma 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 que 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á a este punto en caso de que
la simplificación no nos conduzca a cierto.
Literal DA, 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 ese punto, negado de DA.
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.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed. Click to expand it.
This diff is collapsed. Click to expand it.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment