Docente

• Prof. Agostino Dovier

Indirizzo e-mail
agostino.dovier@uniud.it

Indirizzo Pagina Web Personale
http://www.dimi.uniud.it/dovier

Crediti

6 CFU

Finalità

Lo scopo del corso e' lo studio dei paradigmi di programmazione dichiarativi fondati sul concetto di vincolo e alla loro applicazione concreta a varie tipologie di problemi e, in particolare, alla rappresentazione della conoscenza e al ragionamento su essa. Sara' data particolare enfasi ai linguaggi logici con vincoli su domini finiti, al cosiddetto Answer Set Programming e agli action-description languages adatti a definire problemi di planning. Tali linguaggi vengono oggigiorno utilizzati con successo nella risoluzione di problemi combinatorici, di ottimizzazione, e nella modellazione di sistemi intelligenti, con ricadute multidiciplinari. I paradigmi saranno presentati in modo rigoroso sia per quanto riguarda gli aspetti semantici ed implementativi che sotto il profilo pratico, mediante la codifica e risoluzione di diversi problemi.

Programma

Constraint satisfaction/optimization problems (CSP/COP) e loro sostanziale equivalenza.
NP hardness di semplici CSP. Spazio e alberi di ricerca.
Tecniche naive di ricerca e loro implementazione in Prolog.
Tecniche (note) per risolvere CSP e COP: Local search, e (Integer) Linear Programming SAT e ASP.
Constraint Solver. Risolutori completi ed incompleti. Regole di risoluzione: domain reduction, transformation e introduction. Derivazioni e constraint propagation.
Node consistency, e Arc consistency. Bounds Consistency. Directional Arc/Bounds Consistency.
Hyperarc (e Bounds) consistency. Path Consistency. K-consistency.
Alberi di ricerca: prop labeling trees. Esempi ed effetti della scelta delle variabili sulle dimensioni degli alberi di ricerca. Constraint Programming (vari formalismi).
Richiami di Prolog. Constraint Logic Programming (CLP).
Regola di derivazione e suo insrimento nella SLD risoluzione.
Metodologia constrain & generate in CLP. Esempi di CSP Modeling: N-regine, knapsack, numeri di Schur, circuito hamiltoniano, codici di Hamming, sudoku, protein folding.
Tecniche per la ricerca dell'ottimo in CLP(FD) usando labeling, ricerca bottom-up con timeout, e ricerca locale.
Introduzione ai vincoli globali. Vincoli di all_different.
Richiami sulle tecniche di risoluzione al problema di ricerca di un matching massimale in un grafo bipartito.
Tecniche per il filtering di vincoli all_different.
Richiami sulla semantica osservazionale, modellistica e di punto fisso dei programmi definiti.
Programmi generali. Principali problemi semantici. Direzionalità delle regole.
La negazione in Prolog: CWA e NaF. Esempi e limiti della NaF. Implementazione con cut & fail.
Completamento (regola di Herbrand) e relazioni tra le semantiche.
Completamento di programmi generali. Modelli del completamento e cenno ai modelli well-founded. Grounding.
Modelli stabili. Definizione, primi esempi e NP-completezza del problema dell'esistenza di un modello stabile.
Programmi e codici ASP. Tecniche di programmazione ASP. Codifica di CSP con codici ASP. Alcuni esempi: Graph Coloring, N-Queens, Numeri Schur, Hamilton Circuit, Protein Folding.
Rappresentazione della conoscenza statica e dinamica con ASP: La zebra evasa, La capra e il cavolo.
Rappresentazione e ragionamento sul problema della torre di Hanoi e su quesiti di Smullyan.
Cenni al funzionamento dei principali solver per answer set programming.
Linguaggi per il planning (Action Description Languages).
Sintassi e semantica del linguaggio B. Non determinismo e static laws.
Compilazione di B in ASP e interpretazione di B con CLP(FD). Esempi: La capra e il cavolo, Le tre botti. Approfondimenti su vari aspetti del corso basati su recenti risultati del docente e del suo gruppo.

Bibliografia

- A. Dovier e A. Formisano: Programmazione Dichiarativa con Prolog, CLP, ASP, e CCP. Disponibile on line.

- Krzysztof R. Apt and Mark Wallace. Constraint Logic Programming using Eclipse. Cambridge University Press, 2007

- Chitta Baral. Knowledge representation, reasoning and declarative problem solving, Cambridge University Press, 2003

- Altro materiale on-line disponibile dal sito del corso.

Modalità d'esame

Progetto e orale su appuntamento.