ID:
70454
Tipo Insegnamento:
Opzionale
Durata (ore):
60
CFU:
6
SSD:
SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Url:
INGEGNERIA INFORMATICA E DELL’AUTOMAZIONE/Percorso Comune Anno: 2
Anno:
2024
Dati Generali
Periodo di attività
Secondo Semestre (24/02/2025 - 05/06/2025)
Syllabus
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) e Answer Set Programming
- 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
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) e Answer Set Programming
- 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
• programmazione logica
• problemi di soddisfacimento di vincoli e loro tecniche di risoluzione
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 risolutori SAT e di Answer Set Programming per la risoluzione di problemi a vincoli.
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 risolutori SAT e di Answer Set Programming per la risoluzione di problemi a vincoli.
Verifica 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 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.
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 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
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
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
Contenuti
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.
Programmazione logica a vincoli sui domini finiti
- Vincoli globali
- Ottimizzazione
- Generazione di nuovi vincoli
- rimozione di simmetrie, vincoli ridondanti
- strategie di search
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
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.
Programmazione logica a vincoli sui domini finiti
- Vincoli globali
- Ottimizzazione
- Generazione di nuovi vincoli
- rimozione di simmetrie, vincoli ridondanti
- strategie di search
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
Lingua Insegnamento
ITALIANO
Corsi
Corsi
INGEGNERIA INFORMATICA E DELL’AUTOMAZIONE
Laurea Magistrale
2 anni
No Results Found
Persone
Persone
No Results Found