7. Algoritmo DPLL
Se utiliza para resolver el problema de satisfactibilidad booleana.
- El algoritmo DPLL descompone problemas complejos en subproblemas más simples, utilizando una estrategia de búsqueda con retroceso.
- Se comienza con una solución parcial y se busca una solución completa, retrocediendo cuando es necesario.
simplificación de fórmulas
- Se simplifican las fórmulas asumiendo valores de verdad para las variables, eliminando cláusulas o literales según corresponda.
- Se definen conceptos como cláusula unitaria (contiene solo una literal) y literal pura (aparece con el mismo signo en todas las cláusulas).
pasos del algoritmo DPLL
- El algoritmo tiene varios pasos, incluyendo la verificación de casos base, la simplificación con cláusulas unitarias y literales puras, y la selección de variables arbitrarias.
- Se ilustra el uso del algoritmo a través de un ejemplo práctico relacionado con un homicidio en un tren, mostrando cómo se aplica la simplificación y se determina la satisfactibilidad.
Las literales mencionadas en el video son las variables booleanas que pueden tomar valores de verdad (verdadero o falso) en el contexto de las fórmulas lógicas. Aquí hay un resumen de los tipos de literales:
-
Literal Afirmada: Es una variable que se considera verdadera. Por ejemplo, si A es una literal afirmada, se asume que A es verdadera.
-
Literal Negada: Es una variable que se considera falsa. Por ejemplo, si ¬A (no A) es una literal negada, se asume que A es falsa.
En el contexto del algoritmo DPLL, las literales se utilizan para simplificar las fórmulas y determinar la satisfactibilidad de las mismas.
Una literal pura es un concepto importante en el contexto del algoritmo DPLL y la satisfactibilidad booleana. En términos simples, una literal pura es una variable que aparece con el mismo signo en todas las cláusulas de una fórmula. Esto significa que, si tienes una variable, por ejemplo, "A", y siempre aparece como "A" (verdadera) en todas las cláusulas, entonces "A" es una literal pura.
FNC = Formula Normal Conjuntiva
relatedInteligencia Artificial