PDF de programación - Tema 3: Algoritmos para SAT

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Tema 3:

Algoritmos para SAT

Dpto. Ciencias de la Computación Inteligencia Artificial

Universidad de Sevilla

Lógica Informática

(Tecnologías Informáticas)

Curso 2015–16

Contenido

Introducción

Tableros semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de Davis–Putnam
Estructura del algoritmo
Ejemplos

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Introducción

Presentaremos dos algoritmos para estudiar la

satisfactibilidad de un conjunto de fórmulas
proposicionales:

El método de tableros semánticos, y
El algoritmo DPLL

(Davis–Putnam–Logemann-Loveland)

Ambos están basados en una búsqueda sistemática de

modelos.

En ambos casos la búsqueda suele representarse

gráficamente mediante un árbol.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Tableros vs DPLL

Tienen características propias que distinguen claramente
ambos métodos:

Algoritmo DPLL:

No trabaja con fórmulas arbitrarias sino sobre conjuntos

de cláusulas. Es preciso “preprocesar” el conjunto de
fórmulas, pasándolo a forma clausal.

Está entre los algoritmos más eficientes para la lógica
proposicional, pero no se extiende fácilmente a otras
lógicas.

Tableros semánticos:

Trabaja directamente sobre el conjunto de fórmulas

proposicionales.

No es tan eficiente como DPLL, pero es muy flexible y

puede adaptarse a otras lógicas (como la lógica de
primer orden, lógicas descriptivas, modales, etc.).

Resulta útil en el estudio teórico de diversas lógicas,

para probar propiedades formales como la completitud.

Tableros Semánticos

Gracias a la FND sabemos que la satisfactibilidad de
una fórmula puede reducirse a la de ciertos conjuntos
de literales.

El método de los tableros semánticos organiza de

manera sistemática la búsqueda de modelos, reduciendo
la satisfactibilidad de las fórmulas consideradas a la de
ciertos conjuntos de literales.

El método de tableros semánticos:

1. Clasifica las fórmulas en dos clases:

Las fórmulas α, que se comportan como conjunciones
Las fórmulas β, que se comportan como disyunciones

2. Asocia a cada fórmula, F , otras dos fórmulas más

sencillas (sus componentes) de modo que la
satisfactibilidad de F se reduce a la de sus componentes.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Fórmulas de tipo α

Las fórmulas de tipo α son las siguientes:

α
¬¬F
F1 ∧ F2
¬(F1 ∨ F2)
¬(F1 → F2)
F1 ↔ F2

α1
F
F1
¬F1
F1

α2

F2
¬F2
¬F2

F1 → F2 F2 → F1

Las fórmulas α1 y α2 son las componentes de α.
Si F es de tipo α, entonces F ≡ α1 ∧ α2.
Para satisfacer una fórmula de tipo α es necesario y

suficiente satisfacer simultáneamente sus dos
componentes α1 y α2.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Fórmulas de tipo β

Las fórmulas de tipo β son las siguientes:

β

F1 ∨ F2
¬(F1 ∧ F2)
(F1 → F2)
¬(F1 ↔ F2) ¬(F1 → F2) ¬(F2 → F1)

β1
F1
¬F1
¬F1

β2
F2
¬F2
F2

Las fórmulas β1 y β2 son las componentes de β.
Si F es de tipo β, entonces F ≡ β1 ∨ β2
Para satisfacer una fórmula de tipo β sólo es necesario
y suficiente satisfacer una de sus componentes β1 y β2.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Reglas α y β

Reducen la consistencia de un conjunto de fórmulas U a la
de otro conjunto U formado por fórmulas más sencillas.

Regla α: Si F ∈ U es de tipo α, entonces

U satisfactible ⇐⇒ (U−{F})∪{α1, α2} satisfactible

Regla β: Si F ∈ U es de tipo β, entonces

U satisfactible ⇐⇒



(U − {F}) ∪ {β1} satisfactible

o
(U − {F}) ∪ {β2} satisfactible

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Ejemplo
La fórmula q ∧ p ∧ (p → (q → ¬p)) es insatisfactible:

q ∧ p ∧ (p → (q → ¬p))

q, p ∧ (p → (q → ¬p))

q, p, ¬p

q, p, (p → (q → ¬p))

HHHHH
q, p, q → ¬p
×
HHH

q, p, ¬q
q, p, ¬p
×
×

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Construcción de un tablero completo
Un tablero para {A1, . . . , An} es un árbol T , con nodos
etiquetados por conjuntos de fórmulas, tal que:

La raíz r de T está etiquetado por U(r ) = {A1, . . . An}.
Para cada hoja l de T , con etiqueta U(l), no marcada,

hacer:

1. Si U(l) es un conjunto de literales, entonces:

marcar con × (y se denomina hoja cerrada).

1.1 Si existe un par de literales complementarios en U(l),
1.2 Si no existe tal par, marcar con (hoja abierta).

2. Si U(l) no es un conjunto de literales, elegir A de U(l)

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

no literal.
2.1 Si A es una α–fórmula, entonces añadir un hijo l de l

con U(l) = (U(l) \ {A}) ∪ {α1, α2} (α2 puede no
existir).

2.2 Si A es una β–fórmula, entonces añadir dos hijos l, l

con etiquetas



) = (U(l)\{A})∪{β1} y U(l



) = (U(l)\{A})∪{β2}

U(l

Propiedades de los tableros completos

La construcción siempre termina. El tablero final se

denomina tablero completo.

Un tablero T es cerrado si todas sus hojas son

cerradas. En otro caso es abierto.

Teorema. (Corrección y Completitud)
Sea S un conjunto de fórmulas y T un tablero completo
para S.

1. Corrección: Si T es cerrado, entonces S es

insatisfactible.

2. Completitud: Si S es insatisfactible, entonces T es

cerrado.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Extrayendo modelos de un tablero completo
Un conjunto de fórmulas {A1, . . . , An} admite un
tablero completo abierto si y sólo si es un conjunto
satisfactible.

Además cada rama abierta del tablero completo define

Si U es la etiqueta de una hoja abierta, podemos

un modelo.
obtener un modelo v del conjunto {A1, . . . , An}, como
sigue

v (p) = 1 si p ∈ U ó ¬p /∈ U, y
v (p) = 0 si ¬p ∈ U.

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Extrayendo modelos de un tablero completo (II)

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

p ∧ ¬q ∧ (p → ((q ∨ r ) → (p ∧ r )))

p, ¬q ∧ (p → ((q ∨ r ) → (p ∧ r )))

p, ¬q, p → ((q ∨ r ) → (p ∧ r ))

p, ¬q, ¬p

×



HHHHHHH
p, ¬q, (q ∨ r ) → (p ∧ r )
HHHHH

p, ¬q, ¬(q ∨ r )

p, ¬q, ¬r



p, ¬q, p ∧ r
p, ¬q, r



Induce v (p) = v (r ) = 1, v (q) = 0

Tableros completos y FND

Un tablero completo para una fórmula F puede

utilizarse para obtener una FND de F .

Si T es un tablero completo para F , procedemos como

sigue:

1. Si U1,. . . , Uk son los conjuntos de literales que

etiquetan las hojas abiertas de T , formamos para cada
Uj una conjunción, Cj , con todos los literales de Uj .

2. Una FND de F se obtiene formando la disyunción

C1 ∨ ··· ∨ Ck .

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Tableros y FND: Ejemplo
Si F es la fórmula q ∧ s ∧ (q → (r → ¬p))

q ∧ s ∧ (q → (r → ¬p))

q, s ∧ (q → (r → ¬p))

q, s, ¬q

q, s, (q → (r → ¬p))

HHHHH
q, s, r → ¬p
×
HHH

q, s, ¬p



q, s, ¬r

Una FND de F es (q ∧ s ∧ ¬r ) ∨ (q ∧ s ∧ ¬p).

Algoritmos para

SAT

Introducción

Tableros
semánticos
Fórmulas α y β
Tableros completos
Búsqueda de modelos
Formas normales
Consecuencia lógica

Algoritmo de
Davis–Putnam
Estructura del
algoritmo
Ejemplos

Tableros y FNC

Para obtener una FNC de una fórmula F nos basamos
Si G es una FND de ¬F , aplicando a ¬G las leyes de

en la siguiente observación:

De Morgan y eliminación de negaciones dobles
transformamos ¬G en una FNC de