PDF de programación - Tema 5: Aplicaciones de los algoritmos para SAT

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Tema 5:

Aplicaciones de los 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

Ejemplos de Aplicación

Prover9 y Mace4
El problema de los mentirosos
El problema de los rectángulos
El problema de las 4 reinas
Sudoku

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Prover9 y Mace4

Prover9 es un demostrador automático para las lógicas

proposicionales y de primer orden.

Mace4 es un calculador de modelos.
Disponen de un interfaz gráfico. Son libres y se pueden

descargar en:
http://www.cs.unm.edu/∼mccune/mace4

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de los 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 da la siguiente información:

A dice ”B y C son veraces si y sólo si C es veraz”
B dice ”Si A y C son veraces, entonces B y C son

veraces y A es mentiroso”

C dice ”B es mentiroso si y sólo si A o B es veraz”

Determinar a qué tribu pertenece cada uno.

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de los mentirosos

Formalización: a, b y c representan que A, B y C son
veraces (en consecuencia, ¬a, ¬b y ¬c representan que
A, B y C son mentirosos).

Representación:

a ↔ (b ∧ c ↔ c)

b ↔ (a ∧ c → b ∧ c ∧ ¬a)

c ↔ (¬b ↔ a ∨ b)

Resultado del cálculo de modelos con Mace4:

v (a) = 1, v (b) = 1, v (c) = 0

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

El problema de los mentirosos
Si añadimos a ∧ b ∧ ¬c como objetivo, y usamos Prover9
para encontrar una demostración:

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de los rectángulos

Enunciado: Un rectángulo se divide en seis rectángulos
menores como se indica en la figura. Demostrar que si cada
una de los rectángulos menores tiene un lado cuya medida es
un número entero, entonces la medida de alguno de los lados
del rectángulo mayor es un número entero.

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Formalización:

base: la base del rectángulo mayor es un número entero
altura: la altura del rectángulo mayor es un número

entero

basex : la base del rectángulo x es un número entero
alturax : la altura del rectángulo x es un número entero

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de los rectángulos

Representación:

baseA ∨ alturaA, baseB ∨ alturaB , baseC ∨ alturaC
baseD ∨ alturaD, baseE ∨ alturaE , baseF ∨ alturaF

baseA ↔ baseC , baseA ∧ baseD → baseF

baseD ∧ baseE → baseB , baseA ∧ baseB → base

alturaD ∧ alturaF → alturaE

alturaA ∧ alturaC ∧ alturaF → altura
alturaB ∧ alturaD ∧ alturaF → altura

alturaB ∧ alturaE → altura

Objetivo: base ∨ altura
Prover9: THEOREM PROVED

El problema de las 4 reinas

Enunciado: Calcular las formas de colocar 4 reinas en un
tablero de 4x4 de forma que no se ataquen entre sí (no haya
más de una reina en cada fila, columna o diagonal).

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Formalización: rij (1 ≤ i, j ≤ 4) indica que hay una reina en
la fila i columna j

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de las 4 reinas

En cada fila hay una reina:

r11 ∨ r12 ∨ r13 ∨ r14, r21 ∨ r22 ∨ r23 ∨ r24
r31 ∨ r32 ∨ r33 ∨ r34, r41 ∨ r42 ∨ r43 ∨ r44

Si en una casilla hay reina, entonces no hay más reinas en su
fila, su columna y sus diagonales:
r11 → (¬r12∧¬r13∧¬r14)∧(¬r21∧¬r31∧¬r41)∧(¬r22∧¬r33∧¬r44)
r12 → (¬r11∧¬r13∧¬r14)∧(¬r22∧¬r32∧¬r42)∧(¬r21∧¬r23∧¬r34)
r13 → (¬r11∧¬r12∧¬r14)∧(¬r23∧¬r33∧¬r43)∧(¬r31∧¬r22∧¬r24)
r14 → (¬r11∧¬r12∧¬r13)∧(¬r24∧¬r34∧¬r44)∧(¬r23∧¬r32∧¬r41)
r21 → (¬r22∧¬r23∧¬r24)∧(¬r11∧¬r31∧¬r41)∧(¬r32∧¬r43∧¬r12)
r22 → (¬r21∧¬r23∧¬r24)∧(¬r12∧¬r32∧¬r42)∧(¬r11∧¬r33∧¬r44∧¬r13∧¬r31)
r23 → (¬r21∧¬r22∧¬r24)∧(¬r13∧¬r33∧¬r43)∧(¬r12∧¬r34∧¬r14∧¬r32∧¬r41)
r24 → (¬r21∧¬r22∧¬r23)∧(¬r14∧¬r34∧¬r44)∧(¬r13∧¬r33∧¬r42)

El problema de las 4 reinas

Algoritmos para

SAT

Si en una casilla hay reina, entonces no hay más reinas en su
fila, su columna y sus diagonales:
r31 → (¬r32∧¬r33∧¬r34)∧(¬r11∧¬r21∧¬r41)∧(¬r42∧¬r13∧¬r22)
r32 → (¬r31∧¬r33∧¬r34)∧(¬r12∧¬r22∧¬r42)∧(¬r21∧¬r43∧¬r14∧¬r23∧¬r41)
r33 → (¬r31∧¬r32∧¬r34)∧(¬r13∧¬r23∧¬r43)∧(¬r11∧¬r22∧¬r44∧¬r24∧¬r42)
r34 → (¬r31∧¬r32∧¬r33)∧(¬r14∧¬r24∧¬r44)∧(¬r12∧¬r23∧¬r43)
r41 → (¬r42∧¬r43∧¬r44)∧(¬r11∧¬r21∧¬r31)∧(¬r14∧¬r23∧¬r32)
r42 → (¬r41∧¬r43∧¬r44)∧(¬r12∧¬r22∧¬r32)∧(¬r31∧¬r24∧¬r33)
r43 → (¬r41∧¬r42∧¬r44)∧(¬r13∧¬r23∧¬r33)∧(¬r21∧¬r32∧¬r34)
r44 → (¬r41∧¬r42∧¬r43)∧(¬r14∧¬r24∧¬r34)∧(¬r11∧¬r22∧¬r33)

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

El problema de las 4 reinas

Búsqueda de modelos con Mace4:

r11 : 0, r12 : 0, r13 : 1, r14 : 0

r21 : 1, r22 : 0, r23 : 0, r24 : 0

r31 : 0, r32 : 0, r33 : 0, r34 : 1

r41 : 0, r42 : 1, r43 : 0, r44 : 0

r11 : 0, r12 : 1, r13 : 0, r14 : 0

r21 : 0, r22 : 0, r23 : 0, r24 : 1

r31 : 1, r32 : 0, r33 : 0, r34 : 0

r41 : 0, r42 : 0, r43 : 1, r44 : 0

Algoritmos para

SAT

Ejemplos de
Aplicación
Prover9 y Mace4
El problema de los
mentirosos
El problema de los
rectángulos
El problema de las 4
reinas
Sudoku

Sudoku

Problema: Resolver sudokus.
Descripción del problema:

Un sudoku estás dado por un tablero de 9 × 9 casillas,

dividido a su vez en 3 × 3 subtableros de 3 × 3.

7
2

8

1

7

2

6
3
4

3

5

7

1

8

4

6

3

Cada casilla puede contener un número del 1 al 9.
Inicialmente se proporcionan los números que ocupan
algunas de las casillas. El juego consiste en rellenar el
resto de casillas de modo que cada fila, cada columna y
cada subtablero contenga todos los números del 1 al 9.