PDF de programación - Tema 6: Algoritmos para SAT. Aplicaciones - Lógica matemática y fundamentos (2016–17)

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Lógica matemática y fundamentos (2016–17)

Tema 6: Algoritmos para SAT. Aplicaciones

José A. Alonso Jiménez
María J. Hidalgo Doblado

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

1 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Tema 6: Algoritmos para SAT. Aplicaciones

1. Algoritmos para SAT

2. Aplicaciones

2 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Tema 6: Algoritmos para SAT. Aplicaciones

1. Algoritmos para SAT
Equiconsistencia
Eliminación de tautologías
Eliminación unitaria
Eliminación de literales puros
Regla de división
Algoritmo DPLL

2. Aplicaciones

3 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Equiconsistencia

Equiconsistencia

Notación:

Ejemplos:

{{p}} ≈ {{p},{q}}
{{p}} 6≈ {{p},{¬p}}

Literales: L, L0, L1, L2, . . .
Cláusulas: C , C0, C1, C2, . . .
Conjuntos de cláusulas: S, S0, S1, S2, . . .

Def. S y S0 son equiconsistentes (y se representa por S ≈ S0) si

S es consistente syss S0 es consistente

4 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Eliminación de tautologías

Eliminación de tautologías

Prop.: Sean S un conjunto de cláusulas y C ∈ S una tautología.

Entonces, S ≈ S \ {C}.

Ejemplo: {{p, q},{p, q,¬p}} ≈ {{p, q}}.

5 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT
Eliminación unitaria

Eliminación unitaria

Def.: Una cláusula C es unitaria si C tiene sólo un literal.
Def.: Sean S un conjunto de cláusulas y {L} una cláusula

unitaria de S. Entonces la eliminación unitaria de L en S es el
conjunto obtenido borrando en S todas las cláusulas que
contienen L y borrando Lc en todas las cláusulas; es decir,
elimacionUnitaria(S, L) = {C − {Lc} : C ∈ S, L 6∈ C}

Ejemplo: elimacionUnitaria({{p, q},{p,¬q},{¬p},{r}},¬p) =
Prop.: Sean S un conjunto de cláusulas y {L} una cláusula

{{q},{¬q},{r}}
unitaria de S. Entonces S ≈ eliminacionUnitaria(S, L).

Ejemplos:

{{p, q,¬r},{p,¬q},{¬p},{r , u}}

≈ {{q,¬r},{¬q},{r , u}}
≈ {{¬r},{r , u}}
≈ {{u}}

6 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Eliminación de literales puros

Eliminación de literales puros

Def.: L es un literal puro de S si S es un literal de alguna cláusula
de S y el complementario de L no pertenece a las cláusulas de S.

Ejemplos:

p es un literal puro de {{p, q},{p,¬q},{r , q},{r ,¬q}}.
q no es un literal puro de {{p, q},{p,¬q},{r , q},{r ,¬q}}.

Def.: Sean S un conjunto de cláusulas. Entonces la eliminación
del literal puro L de S es el conjunto obtenido borrando en S las
cláusulas que tienen L; es decir,

elimacionPuro(S, L) = {C ∈ S : L 6∈ C}

Prop.: Sean S un conjunto de cláusulas y L un literal puro de S.

Entonces S ≈ eliminacionPuro(S, L).

Ejemplo:

{{p, q},{p,¬q},{r , q},{r ,¬q}}

≈ {{r , q},{r ,¬q}}
≈ {}

7 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT
Regla de división

Regla de división

Prop.: Sea L un literal del conjunto de cláusulas S. Entonces, son

equivalentes
1. S es consistente,
2. (S ∪ {{L}}) ó (S ∪ {{Lc}}) es consistente,
3. elimacionUnitaria(S, L) ó elimacionUnitaria(S, Lc) es consistente,

8 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Algoritmo DPLL

El algoritmo DPLL (Davis, Putnam, Logemann y Loveland)

Entrada: Un conjunto de cláusulas S.
Salida: “Consistente”, si S es consistente e “Inconsistente”, en

caso contrario.

Procedimiento DPLL(S)

1. Si ∈ S, entonces “Inconsistente”.
2. Si S = ∅, entonces “Consistente”.
3. Si S tiene alguna cláusula unitaria {L}, entonces

DPLL(eliminacionUnitaria(S, L).

4. Si S tiene algún literal puro L, entonces

DPLL(eliminacionPuro(S, L)).

5. Sea L un literal de S.

Si DPLL(S ∪ {L})) = “Consistente”, entonces devolver
en caso contrario DPLL(S ∪ {Lc}).

“Consistente”;

9 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Algoritmo DPLL

Ejemplo del algoritmo DPLL
S = {{a, b},{¬a, b},{a,¬b},{a,¬d},{¬a,¬b,¬c},{b,¬c},{c,¬f },{f }}

[Unitaria {f }]
[Unitaria {c}]
[Unitaria {b}]
[Unitaria {¬a}]

≈ {{a, b},{¬a, b},{a,¬b},{a,¬d},{¬a,¬b,¬c},{b,¬c},{c}}
≈ {{a, b},{¬a, b},{a,¬b},{a,¬d},{¬a,¬b},{b}}
≈ {{a},{a,¬d},{¬a}}
≈ {,{¬d}}

Por tanto, S es inconsistente.

10 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Algoritmo DPLL

Ejemplo del algoritmo DPLL
S = {{p, q},{¬q},{¬r}} [Unitaria {¬q}]

≈ {{p},{¬r}}
≈ {{¬r}}
∅

Por tanto

[Puro p]
[Puro ¬r]

S es consistente.
Un modelo es I con I(p) = 1, I(q) = 0 e I(r) = 0.

11 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Algoritmos para SAT

Algoritmo DPLL

Ejemplo del algoritmo DPLL
Sea S = {{¬q, r},{¬r , p},{¬r , q},{¬p, q, r},{p, q},{¬p,¬q}} No tiene
cláusulas unitarias ni literales puros. Elegimos el literal p para dividir los casos.

Primer caso:

Segundo caso:

S ∪ {p}
= {{¬q, r},{¬r , p},{¬r , q},{¬p, q, r},{p, q},{¬p,¬q},{p}} [Unit. {p}]
≈ {{¬q, r},{¬r , q},{q, r},{¬q}}
[Unit. {¬q}]
≈ {{¬r},{r}}
[Unit. {r}]
≈ {}
S ∪ {¬p}
= {{¬q, r},{¬r , p},{¬r , q},{¬p, q, r},{p, q},{¬p,¬q},{¬p}} [Unit. {¬p}]
≈ {{¬q, r},{¬r},{¬r , q},{q}}
[Unit. {¬r}]
≈ {{¬q},{q}}
[Unit. {¬q}]
≈ {}

Por tanto, S es inconsistente.

12 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

Tema 6: Algoritmos para SAT. Aplicaciones

1. Algoritmos para SAT

2. Aplicaciones

Sobre Prover9 y Mace4
El problema de los veraces y los mentirosos
El problema de los animales
El problema del coloreado del pentágono
El problema del palomar
El problema de los rectángulos
El problema de las 4 reinas
El problema de Ramsey

13 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

Sobre Prover9 y Mace4

Sobre Prover9 y Mace4

Prover9 es un demostrador automático para la lógica de primer

orden.

Mace4 un calculador de modelos.
Prover9 y Mace4 son libres y se encuentran en

http://www.cs.unm.edu/~mccune/mace4

Sintaxis (como la de APLI2):

Usual
Prover9/Mace4

¬ ∧ ∨ → ↔
-
<->

->

&

|

14 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los veraces y los mentirosos

El problema de mentirosos

Enunciado: En una isla hay dos tribus, la de los veraces (que
siempre dicen la verdad) y la de los mentirosos (que siempre
mienten). Un viajero se encuentra con tres isleños A, B y C y
cada uno le dice una frase

A dice “B y C son veraces syss C es veraz”
B dice “Si A y B son veraces, entonces B y C son veraces y A es

mentiroso”

C dice “B es mentiroso syss A o B es veraz”
Determinar a qué tribu pertenecen A, B y C.

Simbolización:

a, b y c representan que A, B y C son veraces
-a, -b y -c representan que A, B y C son mentirosos

15 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los veraces y los mentirosos

El problema los mentirosos

Idea: las tribus se determinan a partir de los modelos del
conjunto de fórmulas correspondientes a las tres frases.

Representación en Mace4 (pb_mentirosos.in)

formulas(assumptions).

a <-> (b & c <-> c).
b <-> (a & c -> b & c & -a).
c <-> (-b <-> a | b).

end_of_list.

16 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los veraces y los mentirosos

El problema de los mentirosos
Cálculo de modelos con Mace4

> mace4 -N2 -m9 -p1 <pb_mentirosos.in

a : 1
b : 1
c : 0

Conclusión: A y B son veraces y C es mentiroso.

17 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los veraces y los mentirosos

El problema de los mentirosos

Representación en Prover9 (pb_mentirosos_2.in)

formulas(assumptions).

a <-> (b & c <-> c).
b <-> (a & c -> b & c & -a).
c <-> (-b <-> a | b).

end_of_list.

formulas(goals).

a & b & -c.
end_of_list.

18 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los veraces y los mentirosos

El problema de los mentirosos

Demostración con Prover9:

> prover9 <pb_mentirosos_2.in >pb_mentirosos_2.out

[assumption].
[goal].

1 a <-> (b & c <-> c).
[assumption]
2 b <-> (a & c -> b & c & -a). [assumption]
3 c <-> (-b <-> a | b).
4 a & b & -c.
5 -a | b | -c.
6 a | c.
9 b | a.
10 b | c.
11 -c | -b.
12 -a | -b | c.
13 b | -a.
14 -b | a.
15 a.
16 b.
17 c.
18 $F.
============================== end of proof ==========================
THEOREM PROVED

[clausify(1)].
[clausify(1)].
[clausify(2)].
[clausify(2)].
[clausify(3)].
[deny(4)].
[10,5]
[11,6].
[14,9].
[13,15].
[12,15,16].
[11,17,16].

19 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los animales

El problema de los animales

Enunciado: Disponemos de una base de conocimiento compuesta

de reglas sobre clasificación de animales y hechos sobre
características de un animal.

Regla 1: Si un animal es ungulado y tiene rayas negras, entonces

Regla 2: Si un animal rumia y es mamífero, entonces es ungulado.
Regla 3: Si un animal es mamífero y tiene pezuñas, entonces es

es una cebra.

ungulado.

Hecho 1: El animal tiene es mamífero.
Hecho 2: El animal tiene pezuñas.
Hecho 3: El animal tiene rayas negras.

Demostrar a partir de la base de conocimientos que el animal es
una cebra.

20 / 49

LMF Tema 6: Algoritmos para SAT. Aplicaciones

Aplicaciones

El problema de los animales

El problema de los animales

Representación en Prover9 (pb_animales.in)

formulas(assumptions).

es_ungulado & tiene_rayas_negras -> es_cebra.
rumia & es_mamifero -> es_ungulado.
es_mamifero & tie