LI2012: Algoritmos SAT. Aplicaciones de la lógica proposicional
En la primera parte de la clase de hoy del curso Lógica Informática
hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland).
En la seguna parte, hemos visto cómo resolver lógicamente problemas representándolos en la lógica proposicional y usando Prover9/Mace4 para su solución.
Los problemas que se han visto son
- 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.
Las transparencias utilizadas son las del tema 6
Read More “LI2012: Algoritmos SAT. Aplicaciones de la lógica proposicional”