CONSTRAINT PROGRAMMING
Anno accademico e docente
Non hai trovato la Scheda dell'insegnamento riferita a un anno accademico precedente?
Ecco come fare >>
- English course description
- Anno accademico
- 2018/2019
- Docente
- MARCO GAVANELLI
- Crediti formativi
- 6
- Periodo didattico
- Secondo Semestre
- SSD
- ING-INF/05
Obiettivi formativi
- L'obiettivo principale del corso consiste nel fornire allo studente la conoscenza dei principali linguaggi di programmazione dichiarativi fondati sul concetto di vincolo e nel mettere gli studenti in grado di modellare problemi a vincoli nei principali linguaggi a vincoli.
Il corso presenta le principali tecniche di propagazione e risoluzione dei vincoli e la loro applicazione concreta a varie tipologie di problemi reali.
In particolare, il corso tratta i linguaggi e risolutori sui domini finiti, con cenni di linguaggi e risolutori sui reali. Particolare enfasi verra` data ai linguaggi basati sulla logica, ovvero linguaggi di programmazione logica a vincoli e programmazione Answer Set Programming. Verranno poi spiegate le principali tecniche utilizzate nei risolutori SAT e le tecniche di codifica di problemi a vincoli in SAT. Verranno mostrati linguaggi di linguaggi di modellazione di problemi a vincoli, quali MiniZinc.
Le principali conoscenze acquisite sono relative a:
• tecniche di risoluzione di vincoli
• linguaggi di programmazione e di modellazione a vincoli
• modellazione di problemi in linguaggi logici e a vincoli
Le principali abilità (ossia la capacità di applicare le conoscenze acquisite) sono:
• risoluzione di un problema tramite un modello a vincoli in diversi linguaggi basati sulla logica Prerequisiti
- E’ necessario avere acquisito e assimilato le seguenti conoscenze fornite dal corso "Fondamenti di Intelligenza Artificiale”:
• programmazione logica
• problemi di soddisfacimento di vincoli e loro tecniche di risoluzione Contenuti del corso
- Il corso prevede 60 ore di didattica frontale parte in aula e parte in laboratorio, sui seguenti argomenti principali:
Programmazione logica a vincoli
Il linguaggio MiniZinc
Algoritmi di risoluzione SAT e di codifica in SAT
Answer Set Programming Metodi didattici
- Il corso è diviso in 60 ore di lezione parte in aula e parte nel laboratorio di informatica.
Le lezioni riguardano gli argomenti del corso e includono esercitazioni guidate al calcolatore.
Le esercitazioni in laboratorio riguardano l'uso di linguaggi di programmazione logica a vincoli, di MiniZinc, di risolutori SAT e di Answer Set Programming per la risoluzione di problemi a vincoli. Modalità di verifica dell'apprendimento
- L'obiettivo della prova d'esame consiste nel verificare il livello di raggiungimento degli obiettivi formativi precedentemente indicati.
Al fine di verificare la capacità dello studente di modellare problemi a vincoli nei vari linguaggi di programmazione studiati, viene fatta una prova di laboratorio; in questa prova, allo studente viene descritto un problema, che lo studente deve poi risolvere tramite un programma in Answer Set Programming oppure in MiniZinc e tramite un programma in programmazione logica a vincoli.
Il totale dei punti disponibili per questa prova è 25; una valutazione intorno al 25 dimostrerà che lo studente ha ottenuto abbia ottime capacità di modellare e risolvere problemi a vincoli, mentre uno studente che ottiene intorno a 13 punti dimostrerà di aver ottenuto sufficienti capacità di modellare e risolvere problemi a vincoli.
Al fine di verificare la conoscenza dello studente sulle tecniche di propagazione disponibili nei risolutori moderni, viene fatta una prova scritta. Questa prova contiene un esercizio in cui lo studente deve dimostrare di aver appreso le tecniche di propagazione con vincoli globali nella programmazione logica a vincoli sui domini finiti (tipicamente da 4 punti) ed un esercizio sulla risoluzione in problemi SAT (tipicamente da 4 punti).
Il voto finale è data dalla somma dei voti nella parte di laboratorio e nella parte di teoria.
Su richiesta, l'esame può essere sostenuto in lingua Inglese Testi di riferimento
- Il materiale didattico di riferimento comprende:
- copie dei lucidi proiettati a lezione, pubblicati sul sito web del corso
- manuali on-line dei software utilizzati (ECLiPSe, MiniZinc, clasp)
Per approfondimenti, si consigliano i seguenti testi:
- Krzysztof R. Apt and Mark Wallace. Constraint Logic Programming using Eclipse. Cambridge University Press, 2007
- Francesca Rossi, Peter van Beek, Toby Walsh (Eds.):
Handbook of Constraint Programming, Elsevier 2006
- Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Torsten Schaub: Answer Set Solving in Practice. Morgan & Claypool, 2012
