Docència
Lògica a la Informàtica (LI) -- Tardor 2009 --
La data límit per a entregar les dues primeres pràctiques és diumenge 20 de desembre.
L'entrega es farà a través del racó de la FIB.
-
Primera pràctica:
S'enviarà un únic arxiu comprimit amb el següent contingut:
- Codi font del SAT solver. El SAT solver ha de dir si la fórmula és satisfactible o no. En cas que ho sigui, cal que retorni un model. Si es requereixen instruccions o llibreries addicionals
per a la seva compilació seran especificades en un arxiu README.
- Petit document amb estadístiques del vostre SAT solver sobre el següent joc de proves, tots ells en format DIMACS . El document ha de contenir l'especificació de la màquina utilizada, i per cada benchmark del joc de proves, la següent informació:
- Resposta del SAT solver (SAT/INSAT)
- Temps en segons (assumiu un temps límit de 600 segons)
- Nombre extensions del model degudes a una decisió arbitrària
- Nombre extensions del model degudes a una propagació unitària
AJUDA: podeu utilitzar aquest parser escrit en C per a llegir el format DIMACS.
Per a depurar el vostre programa podeu provar amb aquests exemples senzills.
A mode orientatiu, en aquest arxiu podeu trobar els resultats obtinguts per un SAT solver MOLT bàsic.
CRITERIS DE VALORACIÓ: es valorarà a parts iguals la llegibilitat del codi i la seva eficiència.
-
Segona pràctica:
La pràctica consisteix en, donat un sudoku en el format del joc de
proves, calcular-ne la solució (o totes les solucions si sabeu com fer-ho!).
Per això es proposen els següents passos:
- Es llegeix l'arxiu que especifica el sudoku i s'escriu en un arxiu la fórmula proposicional corresponent (en format DIMACS ).
- Es converteix el problema a una fórmula 3-SAT amb clàusules unitàries utilitzant el programa proporcionat (to3SAT).
- S'utilitza el vostre propi SAT solver per a llegir la fórmula 3-SAT ( per a la lectura podeu utilitzar l'arxiu llegir_units.c com a base) i com a sortida s'escriurà per pantalla el sudoku amb el mateix format de sortida que el joc de proves però amb les "x" substituïdes pels nombres que pertoquin. NOTA: es pot modificar el SAT solver respecte la primera entrega si ho creieu adient. Si no aconseguiu fer funcionar el vostre SAT solver podeu utilitzar el SAT solver siege, que, en cas de trobar un model l'escriu en l'arxiu siege.results. De totes maneres, utilizar siege es considerarà un demèrit.
Es demana que construïu un programa que llegeixi un sudoku del joc de proves i escrigui per pantalla la seva solució (o totes les possibles solucions si sabeu com fer-ho). Es dóna total llibertat per a integrar les eines que necessiteu (scripts, crides a sistemes des de C, ...). L'únic requeriment és que funcioni sota Linux.
S'enviarà un únic arxiu comprimit amb el codi font de tots els vostres programes, així com instruccions per a la seva utilizació i instal·lació.
En aquest arxiu hi trobareu els jocs de proves i els programes que necessitareu.
CRITERIS DE VALORACIÓ: es valorarà a parts iguals la llegibilitat del codi i la seva eficiència. El càlcul de totes les solucions es considerarà un mèrit addicional però no imprescindible.