Anar al contingut (clic a Intro)
UdG Home UdG Home
Tancar
Menú

Estudia

Dades generals

Curs acadèmic:
2010
Descripció:
Resolució de restriccions. Programació lògica amb restriccions. Resoledors de SAT.
Crèdits:
5
Idioma principal de les classes:
Català
S’utilitza oralment la llengua anglesa en l'assignatura:
Poc (25%)
S’utilitzen documents en llengua anglesa:
Majoritàriament (75%)

Grups

Grup A

Durada:
Semestral, 2n semestre
Professorat:
Miquel Bofill Arasa  / Mateu Villaret Auselle

Altres Competències

  • Ser capaç d'escollir les tècniques i eines de la lògica més adients per resoldre un problema.
  • Ser capaç de modelar problemes complexos.

Continguts

1. Introducció i motivació.

          1.1. Alguns exemples de problemes. Com els resoldríem amb les tècniques vistes a assignatures prèvies? Quant de temps ens costaria? Què en sabríem de les garanties de fiabilitat?

2. Classes de complexitat i reduccions.

          2.1. Algunes classes importants: P, NP, ...

          2.2. Reduccions.

          2.3. Problemes NP-complets i NP-hard.

          2.4. Alguns problemes NP-hard: Programació entera, Pseudo-booleans (0-1 integer programming), 3-SAT, ...

3. Recordatori de lògica proposicional i de lògica de primer ordre.

          3.1. Sintaxi i semàntica.

          3.2. Resolució.

4. Programació lògica amb restriccions (Constraint Logic Programming)

          4.1. Repàs de Prolog.

          4.2. CLP(X) i dominis.

          4.3. Maneres de reduir l'espai de cerca.

          4.4. Exemples: assignació de recursos, horaris, ...

          4.5. Cerca de solucions òptimes amb CLP.

5. Tècniques basades en SAT.

          5.1. Sistemes DPLL amb anàlisi de conflictes.

          5.2. Programació per traducció a SAT i ús de les eines associades.

          5.3. Exemples d'aplicacions: problemes d'horaris, etc.

          5.4. Extensions: Max-SAT, All-SAT.

6. SAT mòdul teories (SMT).

          6.1. SMT amb arrays, llistes, enters i reals.

          6.2. Reduccions a SAT. Mètodes eager.

          6.3. Mètodes lazy. DPLL(T).

7. Comparació amb altres tècniques.

          7.1. SAT i Integer Programming (IP).

          7.2. SAT i Constraint Programming (CP).

          7.3. Aplicació de SMT a CSPs i problemes combinatoris d'optimització.

Activitats

Tipus d’activitat Hores amb professor Hores sense professor Total
Elaboració individual de treballs 0 25,00 25,00
Sessió expositiva 25,00 25,00 50,00
Sessió pràctica 25,00 25,00 50,00
Total 50,00 75,00 125

Bibliografia

  • Garey, Michael R., Johnson, David S., 1945- (cop. 1979). Computers and intractability : a guide to the theory of NP-Completeness. New York: W.H. Freeman and Co..
  • Schöning, Uwe (1989). Logic for computer scientists. Birkhäuser. Catàleg
  • Hogger, C.J. (1990). Essentials of logic programming. Oxford : Clarendon Press. Catàleg
  • Apunts i Articles de la web. Recuperat , a Consultar a la web de l'assignatura

Avaluació i qualificació

Activitats d'avaluació:

Descripció de l'activitat Avaluació de l'activitat %
Classes teòriques Exercicis teòrics 25
Classes de laboratori 25
Pràctiques Realització de treballs pràctics 50

Qualificació

Hi haurà un nota de teoria, amb un pes del 50%, obtinguda mitjançant exercicis proposats durant el curs.

La nota de laboratori (50%) s'obtindrà a partir de l'avaluació de les successives entregues dels exercicis a les classes de laboratori.

També es podrà millorar la nota mitjançant l'estudi i presentació d'algun tema del curs.

Observacions

Objectius:
- Introduir l'estudiant a la utilització d'eines basades en la lògica per a la modelització i resolució de problemes complexos, com ara problemes de planificació, scheduling (planificació del temps i els recursos), optimització, verificació de hardware i software, etc.

Habilitats:
- Ser capaç d'escollir les tècniques i eines de programació més adients per resoldre un problema, tant pel que fa al nivell d'expressivitat de la lògica subjacent com de la complexitat del problema deductiu associat.

Assignatures recomanades

  • Fonaments de la intel·ligència artificial
  • Sistemes de reescriptura

Escull quins tipus de galetes acceptes que el web de la Universitat de Girona pugui guardar en el teu navegador.

Les imprescindibles per facilitar la vostra connexió. No hi ha opció d'inhabilitar-les, atès que són les necessàries pel funcionament del lloc web.

Permeten recordar les vostres opcions (per exemple llengua o regió des de la qual accediu), per tal de proporcionar-vos serveis avançats.

Proporcionen informació estadística i permeten millorar els serveis. Utilitzem cookies de Google Analytics que podeu desactivar instal·lant-vos aquest plugin.

Per a oferir continguts publicitaris relacionats amb els interessos de l'usuari, bé directament, bé per mitjà de tercers (“adservers”). Cal activar-les si vols veure els vídeos de Youtube incrustats en el web de la Universitat de Girona.