Teoría | 10: | martes | 08-10h, | A6E02 |
Teoría | 20: | martes | 16-18h, | A6E02 |
Labo | 11: | miércoles | 08-10h, | A5S104 |
Labo | 12: | miércoles | 10-12h, | C6S308 |
Labo | 21: | miércoles | 18-20h, | A5S108 |
Labo | 13: | miércoles | 08-10h, | C6S306 |
Labo | 22: | miércoles | 18-20h, | A5S109 |
Habrá dos exámenes presenciales de labo delante del ordenador. Atención: Este cuatrimestre vuelve a haber semana de exámenes parciales, con examen parcial de teoría de LI y el primer examen de labo de LI.
16 feb | : | practica 1: sat solver |
23 feb | : | practica 1: sat solver |
02 mar | : | practica 2: prolog |
09 mar | : | practica 2: prolog |
16 mar | : | practica 3: codificación en sat |
23 mar | : | practica 3: codificación en sat |
30 mar | : | practica 4: optimización en sat |
01 abr | : | EXAMEN LABO 10:30 - 12:00h |
20 abr | : | practica 4: optimización en sat |
27 may | : | practica 5: prolog avanzado |
04 may | : | practica 5: prolog avanzado |
11 may | : | practica 6: constraint logic programming (clp) |
18 may | : | practica 6: constraint logic programming (clp) |
02 jun | : | EXAMEN LABO 15:00 - 16:30h |
Modifica el SAT solver SAT-alumnes.cpp
para tratar de la manera más eficiente que puedas los ejemplos de
random3SAT.tar.gz.
Tenéis una presentación describiendo el algoritmo
aquí.
Para ello, mejora la heurística de decisión y la velocidad de propagación.
Adjuntamos un
script
que compara la eficiencia de tu solver
con otro, PicoSAT, ejecutando ambos en la misma máquina. Sobre los problemas insatisfactibles de 300 variables, PicoSAT nunca debería
ser más de 20 veces más rápido que tu solver, y es perfectamente posible conseguir ratios de 10 veces, 5 veces, o incluso mejores
(haz make usando el Makefile para compilar).
Tienes que entregar dos archivos: SAT-alumnes.cpp y tiempos.txt, la salida que genera el script.
Véanse los
problemas A,B y C.
Constraint logic programming (clp). Ver primero el video sobre CLP (que dura 25 minutos). Mira clp_Constraints_Backtracking.pl para entender cómo NO generar los constraints en CLP. Después resuelve:
Ver coins.pl: ¿cómo pagar determinada cantidad, usando el mínimo número de monedas de los diversos tipos dados? Solución: coinsSol.pl.
Tomografías: A matrix which contains zeroes and ones gets "x-rayed" vertically and horizontally, giving the total number of ones in each row and column. The problem is to reconstruct the contents of the matrix from this information. Extend the Prolog source of tomografia.pl
Solve letterDice.pl
Completa el problema squares.pl .
Ojo: hay versión nueva con 6 ejemplos. Algunos de los problemas son duros. Pista: usa labeling([ff],Vars). Mira los manuales; esto escoge la siguiente variable a asignar de manera ff: "first fail", primero la variable más restringida, similarmente a como lo hacíamos en nuestro SAT solver.