Sabemos que Σ |= p si y solo si Σ ∪ {¬ p } es inconsistente.
¿Como verificamos si Σ ∪ {¬ p } es inconsistente?
- El método basado en tablas de verdad es demasiado lento.
- Necesitamos un método alternativo que no construya tablas de verdad.
Reducción a clausulas
Notación: Una clausula es una disjuncion de literales.
Ejemplo: p ∨ ¬q ∨ ¬r.
Una formula p esta en CNF si es de la forma C1 ∧ C2 ∧ · · · ∧ Cn,
donde cada Ci es una clausula.
Podemos representar p como {C1, C2, . . . , Cn}. ¿Por que?
Notación: También usamos ≡ para denotar equivalencia entre conjuntos
de formulas
Reducción a clausulas
Toda formula es equivalente a un conjunto de clausulas.
Ejemplo:
(p ∨ q) → r ≡ ¬(p ∨ q) ∨ r
≡ (¬p ∧ ¬q) ∨ r
≡ (¬p ∨ r) ∧ (¬q ∨ r)
≡ {¬p ∨ r, ¬q ∨ r}
Entonces: Nos basta con resolver el problema de satisfacibilidad
para conjuntos de clausulas.
La regla de resolución
¿Como verificamos si un conjunto de clausulas es inconsistente?
Sabemos que Σ es inconsistente si y solo si Σ |= p, donde p es una
contradicción cualquiera.
Entonces: Fijamos una contradicción y lo que hacemos es
verificar si Σ |= .
Notación: Decimos que es la clausula vacía porque una clausula sin
literales no es satisfacible.
La regla de resolución
Para verificar que Σ |= no queremos usar valuaciones, queremos
usar alguna regla sintáctica.
Notación: Si l = p, entonces ¯l = ¬p, y si l = ¬p, entonces ¯l = p.
Dado: clausulas C1, C2, C3, C4 y literal l.
Regla de resolución:
C1 ∨ l ∨ C2
C3 ∨ ¯l ∨ C4
__________________
C1 ∨ C2 ∨ C3 ∨ C4
La regla es correcta: {C1 ∨ l ∨ C2, C3 ∨ ¯l ∨ C4} |= C1 ∨ C2 ∨ C3 ∨ C4
La regla de resolución:Ejemplo
Ejemplo:
¬
p
∨
q
¬
q
∨
r
___________
¬
p
∨
r
Tenemos que: {¬
p
∨ q,
¬
q
∨
r} |
=
¬
p
∨
r
La regla de resolución: Casos particulares
Algunos casos particulares de la regla de resolución:
C
1
∨ l ∨
C2
i
______________
C
1
∨
C2
0 comentarios:
Publicar un comentario