I1M2015: El patrón de divide y vencerás en Haskell

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante divide y vencerás.

La clase comenzó analizando los árboles de ordenación de una lista de números mediante la ordenación por mezcla y la ordenación rápida.

De este análisis se extrae el patrón de resolución de problemas mediante divide y vencerás (DyV) y sus argumentos:

  • cómo reconocer si el problema es elemental,
  • cómo se resuelven los problemas elementales,
  • cómo se descompone un problema y
  • cómo se combinan las soluciones de los subproblemas.

A continuación se implementa el patrón DyV en Haskell, usando su posibilidad de programar en orden superior para abstraer los argumentos del problema.

Finalmente, se aplica el patrón DyV para implementar los algoritmos de ordenación por mezcla y ordenación rápida.

Las transparencias usadas en la clase son las páginas 1-10 del tema 23:

El código del patrón divide y vencerás es
Read More “I1M2015: El patrón de divide y vencerás en Haskell”

I1M2015: Ejercicios sobre la implementación del TAD de grafos mediante listas

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha comentado las soluciones de los ejercicios de la relación 35 que consiste en la implementación del TAD de los grafos mediante lista.

Las soluciones de los ejercicios de la relación es el siguiente
Read More “I1M2015: Ejercicios sobre la implementación del TAD de grafos mediante listas”

LMF2016: Algoritmo DPLL (Davis, Putnam, Logemann y Loveland)

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos hemos estudiado el algoritmo DPLL (Davis, Putnam, Logemann y Loveland) para decidir la consistencia de conjuntos de cláusulas.

En primer lugar se ha explicado el concepto de equiconsistencia. A continuación, las reglas de eliminación de tautologías, de eliminación unitaria, de eliminación de literales puros y la de división. Finalmente, el algoritmo DPLL.

Las transparencias utilizadas son las página 1 a 12 del tema 6.

LMF2016: Estrategias y refinamientos de resolución

En la primera parte de la clase de hoy del curso Lógica matemática y fundamentos hemos continuado la búsqueda de la automatización del razonamiento.

Empezamos con un primer algoritmo de búsqueda de la cláusula vacía: el de saturación y dos mejoras: eliminación de tautologías y de subsumsución.

A continuación, hemos estudiado distintas estrategias cuyo objetivo es mejorar la búsqueda de la refutación por resolución.

Las estrategias estudiadas son la resolución positiva, la resolución negativa, la resolución unitaria, la resolución por entradas y la resolución lineal.

Además, se ha presentado la estrategia por pesos y propagación unitaria.

Finalmente, se ha mostrado el uso de Prover9 para decidir mediante resolución la validez de argumentos

Las transparencias de esta clase son las páginas 18 a 37 del tema 5.