LI2012: Algoritmos SAT. Aplicaciones de la lógica proposicional

PorJosé A. Alonso

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

Los códigos de los ejemplos se encuentran aquí.