Satisfabilidad Lógica PDF

Definiciones Método de resolución Algoritmo de Davis-Putnam Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Satisfabilidad Lógica Carlos Linares...

Definiciones Método de resolución Algoritmo de Davis-Putnam Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Satisfabilidad Lógica Carlos Linares López Grupo de Planificación y Aprendizaje (PLG) Departamento de Informática Escuela Politécnica Superior Universidad Carlos III de Madrid 10 de enero de 2014 Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Algoritmo de Davis-Putnam Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Definiciones Una fórmula proposicional está en Forma Normal Conjuntiva (CNF) si es de la forma: ki N _ ^ lij i=1 j=1 Un literal l consiste en una variable x afirmada (x) o negada (x) Un literal l es puro en F si l no ocurre en ninguna cláusula de F Una tautologı́a es una fórmula proposicional siempre cierta para cualquier asignación de sus expresiones atómicas. Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Algoritmo de Davis-Putnam Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Problema de satisfabilidad Definición 1 El problema de satisfabilidad consiste en encontrar un modelo M que satisfaga F, M |= F Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Propiedades Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Método de resolución Si F es un conjunto de cláusulas y l es pura en F entonces F − l es satisfacible si y sólo si F es satisfacible Definición 2    F −x si x es pura en F C1 ∨ C2 (x ∨ C1 ) ∈ F , (x ∨ C2 ) ∈ F  Res(F , x) =   y (C1 ∨ C2 ) no es tautologia C ∈F x∈ /F  Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Propiedades Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Propiedades El modelo de resolución asegura que el número de variables decrementa: (p∨r ),(p∨s) p,p (r ∨s) {∅} pero no necesariamente el número de cláusulas Si resulta la cláusula vacı́a, {∅}, F no es satisfacible Si F = ∅, F es satisfacible La resolución no genera modelos, pero preserva la satisfabilidad del problema resultante La aplicación directa del método de resolución da lugar al algoritmo de Davis-Putnam Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Algoritmo de Davis-Putnam 1 Elegir un literal l ∈ F 2 Aplicar Res(F , l) y anotar la variable usada y las cláusulas involucradas 3 Si resulta la cláusula vacı́a, detenerse. Problema no Satisfacible 4 Si resulta F = ∅ ir a 5. En otro caso, volver a 1 5 Problema Satisfacible. Considerar la lista de variables y cláusulas en orden inverso, calculando un valor > ó ⊥ para todas las variables involucradas1 1 > y ⊥ significan cierto y falso respectivamente Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo I Considerar el problema de satisfabilidad lógica con las siguientes cláusulas: C1 :(p ∨ q) C2 :(p ∨ r ) C3 :(q ∨ r ) C4 : q y encontrar un modelo M que la satisfaga con el algoritmo de Davis-Putnam (DP) Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo II Paso 0 G0 = {Ci }4i=1 Inicialmente se consideran todas las clausulas varSelect = p varSelect almacena la selección de variables por paso, y layerSeq = G0 \Res(G0 , p) = layerSeq las clausulas G0 \{C3 , C4 , C5 : (q ∨ r )} = {C1 , C2 } Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo III Paso 1 G1 = {Ci }5i=3 Cláusulas pendientes varSelect = r se escoge r layerSeq = G1 \Res(G1 , r ) = nótese que la resolución de C3 G1 \{C4 , C6 : q} = con C5 genera la clausula C6 {C3 , C5 } Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo IV Paso 2 G2 = {C4 , C6 } Cláusulas pendientes varSelect = q Se escoge la última variable q layerSeq = G2 \Res(G2 , q) Problema no Satisfacible La no factibilidad se detecta al intentar resolver C4 : (q) con la variable q que da la cláusula vacı́a {∅} Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo I Considerar el problema de satisfabilidad lógica con las siguientes cláusulas: C1 :(p ∨ q) C5 : (r ∨ s) C2 :(p ∨ r ) C6 : (u ∨ w ) C3 :(q ∨ r ) C7 :(s ∨ u ∨ w ∨ x) C4 : q y encontrar un modelo M que la satisfaga con el algoritmo de Davis-Putnam (DP) Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo II Paso 0 G0 = {Ci }7i=1 Inicialmente se consideran todas las clausulas varSelect = p almacena la selección de p layerSeq = G0 \Res(G0 , p) = y las clausulas implicadas G0 \{C3 , C4 , C5 , C6 , C7 } = {C1 , C2 } La resolución de las cláusulas C1 y C2 genera exactamente la cláusula C3 : (q ∨ r ) Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo III Paso 1 G1 = {Ci }7i=3 Cláusulas pendientes varSelect = u se escoge u layerSeq = G1 \Res(G1 , u) = G1 \{C3 , C4 , C5 } = {C6 , C7 } y se almacenan las clausulas usadas Nótese que la resolución de las cláusulas C6 y C7 genera la cláusula (s ∨ w ∨ w ∨ x) que es una tautologı́a y, por lo tanto, no se añade Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo IV Paso 2 G2 = {C3 , C4 , C5 } Cláusulas pendientes varSelect = q Se escoge q layerSeq = G2 \Res(G2 , q) = nótese que la resolución de C3 G1 \{C5 , C8 : (r )} = y C4 genera C8 {C3 , C4 } y se almacenan las clausulas usadas Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo V Paso 3 G3 = {C5 , C8 } Cláusulas pendientes varSelect = r Se escoge r layerSeq = G3 \Res(G3 , r ) = r es pura en G3 G3 \ ∅ = {C5 , C8 } y se almacenan las clausulas usadas Puesto que r es pura, todas las clausulas que la contienen se eliminan. Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo VI Paso 4: Se consideran los vectores de variables y cláusulas en orden inverso: layerSeq−1 =({C9 }, {C5 , C8 }, {C3 , C4 }, {C6 , C7 }, {C1 , C2 }) varSelect−1 =hs, r , q, u, pi Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Definición Algoritmo de Davis-Putnam Ejemplos Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Ejemplo VII y se calculan por pasos asignaciones (función h) de verdadero o falso a cada variable que satisfagan sólo las clausulas implicadas en cada paso como se muestra en la siguiente tabla: Paso Variable Cláusulas Asignación 4 hsi {C9 } h(s) = ⊥ 3 hr i {C5 , C8 } h(r ) = ⊥ 2 hqi {C3 , C4 } h(q) = ⊥ 1 hui {C6 , C7 } h(u) = >, h(w ) = ⊥, h(x) = ⊥ 0 hpi {C1 , C2 } h(p) = > Cuadro : Generación del modelo Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Algoritmo de Davis-Putnam-Logemann-Loveland Definición 3 Resolución Unitaria: forma de resolución en la que uno de los padres es una cláusula unitaria Sea F un conjunto de fórmulas y p ∈ At donde At es el conjunto de literales de F. F es satisfacible si y sólo si F ∪ {p} es satisfacible o F ∪ {p} es satisfacible Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Algoritmo de Davis-Putnam-Logemann-Loveland Definición 4 Se denomina reducción de una fórmula F por un modelo parcial v a la fórmula resultante Fv = Red(F , v ) en la que se han propagado las asignaciones de v Si el modelo es completo y resulta el conjunto vacı́o, ∅, entonces la fórmula F es satisfacible y el modelo v lo valida Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Pseudocódigo DPLL (F , v ) Entrada: F es la expresión lógica en CNF a satisfacer v es el modelo que se construye Salida: Un modelo v tal que v |= F o ∅ si no existe ninguno if (∅ ∈ F ) return ∅ G = Red(F , v ) if (G = ∅) return v else l = SeleccionarLiteral(G ) return DPLL (F , v ∪ {l}) ∨ (F , v ∪ {l}) Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Ejemplo I Considerar el problema de satisfabilidad lógica con las siguientes cláusulas: C1 :(p ∨ t) C2 :(p ∨ q) C3 :(t ∨ q) y encontrar un modelo M que la satisfaga con el algoritmo de Davis-Putnam-Logemann-Loveland (DPLL) Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Ejemplo II (p ∨ t) ∧ (p ∨ q) ∧ (t ∨ q) {p = >} {p = ⊥} q ∧ (t ∨ q) t ∧ (t ∨ q) {q = >} {q = ⊥} {t = >} {t = ⊥} t {∅} {∅} q {t = >} {t = ⊥} {q = >} {q = ⊥} ∅ {∅} {∅} ∅ Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Ejemplo III DPLL se podrı́a haber detenido con el primer modelo: v1 = {p = >, q = >, t = >} pero si se le permite continuar encontrarı́a todos los modelos adicionales: v2 = {p = ⊥, q = ⊥, t = ⊥} Carlos Linares López Satisfabilidad Lógica  Definiciones Definiciones Método de resolución Pseudocódigo Algoritmo de Davis-Putnam Ejemplo Algoritmo de Davis-Putnam-Logemann-Loveland Propiedades Bibliografı́a Propiedades DPLL es un algoritmo de el primero en profundidad por lo que tiene: Consumo de memoria lineal Consumo de tiempo exponencial en el número de variables Mejoras al algoritmo DPLL: Algoritmo de selección de la próxima variable, SeleccionarLiteral(G ) Aprendizaje de nuevas cláusulas satisfacibles Backjumping (o backtracking no cronológico) Cálculo incremental de la función de reducción Carlos Linares López Satisfabilidad Lógica  Definiciones Método de resolución Algoritmo de Davis-Putnam Algoritmo de Davis-Putnam-Logemann-Loveland Bibliografı́a Bibliografı́a Marek, Victor W. Introduction to Mathematics of Satisfiability CRC Press, 2009 Carlos Linares López Satisfabilidad Lógica