INTELLIGENZA ARTIFICIALE PER L'OTTIMIZZAZIONE VINCOLATA
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
- 2022/2023
- Docente
- MARCO GAVANELLI
- Crediti formativi
- 6
- Periodo didattico
- Secondo Semestre
- SSD
- ING-INF/05
Obiettivi formativi
- L'insegnamento approfondisce algoritmi e linguaggi basati su intelligenza artificiale per risolvere problemi di soddisfacibilità e di ottimizzazione vincolata.
Gli obiettivi formativi del corso sono che gli studenti siano in grado di
- descrivere le principali caratteristiche di linguaggio di programmazione logica a vincoli sui domini finiti (Constraint Logic Programming on Finite Domains - CLP(FD))
- descrivere gli algoritmi di propagazione dei principali vincoli in CLP(FD)
- modellare un problema di soddisfacibilità o di ottimizzazione vincolata nei linguaggi CLP(FD), Answer Set Programming, MiniZinc
- descrivere l'algoritmo di Conflict Directed Clause Learning di un risolutore SAT
- codificare un problema di soddisfacibilità in SAT
- riconoscere quali modelli a vincoli sono più promettenti di altri 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 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 ed altri domini. Particolare enfasi verrà 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 modellazione di problemi a vincoli, quali MiniZinc.
Programmazione logica a vincoli sui domini finiti
- Vincoli globali
- Ottimizzazione
- Generazione di nuovi vincoli
- rimozione di simmetrie, vincoli ridondanti
- strategie di search
Il linguaggio MiniZinc
Algoritmi di risoluzione SAT
- Algoritmo Davis-Putnam-Logeman-Loveland
- Algoritmo Conflict-Directed Clause Learning
Algoritmi di codifica di problemi di soddisfacimento di vincoli in SAT
- direct encoding
- log encoding
- support encoding
Answer Set Programming Metodi didattici
- Le lezioni sono organizzate tramite la tecnica della Flipped Classroom: vengono fornite videolezioni da guardare a casa su tutti gli argomenti del corso.
Le lezioni in presenza sono tenute in laboratorio di informatica; vengono assegnati esercizi che vengono svolti al calcolatore, per poter apprendere tramite "learning by doing" le tecniche apprese nelle videolezioni.
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.
Agli studenti che seguono le lezioni, verranno anche assegnati esercizi, che verranno corretti dal docente. 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.
Durante la prova di laboratorio è possibile accedere alla documentazione dei software studiato nel corso; non è possibile consultare altro materiale (appunti, slide, ecc.).
Il totale dei punti disponibili per questa prova è 25; una valutazione intorno al 25 dimostrerà che lo studente ha ottenuto 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).
Durante la prova scritta non è possibile utilizzare materiale didattico.
Il voto finale è data dalla somma dei voti nella parte di laboratorio e nella parte di teoria.
Se richiesto con almeno una settimana di anticipo, l'esame può essere sostenuto in lingua Inglese. Testi di riferimento
- Il materiale didattico di riferimento viene pubblicato su Google Classroom (codice swtkeqg per il 2022/23)
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
