Constraint Programming & Planning

Programma dell'insegnamento - Corso di laurea in Informatica Magistrale internazionale

 

Docente

Prof. Agostino Dovier

Indirizzo e-mail
agostino.dovier@uniud.it

Indirizzo Pagina Web Personale
Sito Web 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.

**************************************************************************************

Aims

The student will learn the foundations of the modern declarative programming paradigms based on the notion of constraint. Particular emphasis will be given on constraint logic programming, on answer set programming, and on action description languages. Those languages are nowadays successfully employed for encoding optimization problems (e.g. scheduling, timetabling, planning, etc) and knowledge representation and reasoning. Semantics and implementation techniques will be rigorously presented, and the languages will be also studied from a practical point of view in lab.

Program

Constraint Satisfaction/Optimization Problems (CSP/COP) and main techniques used for dealing with them. Constraint solver, basic notions. Global Constraints.
Summary of Horn clauses-based programming languages; Turing completeness and semantics. Logic Programming with Constraints (CLP): Syntax and Semantics. Declarative programming: "Generate & test" vs "Constrain & generate". Constraints over finite domains and their solvers. Some "case studies": N-queens, Map Coloring, puzzles, scheduling problems, computational biology problems, and games. Answer Set Programming: Syntax and Semantics. Using ASP for encoding NP-complete problems. Action Description Languages: encoding of problems and their implementation either in ASP or in Constraint Logic Programming on Finite Domains. Action Description Languages: syntax, semantics, examples and encoding in ASP and CLP.

References

- A. Dovier e A. Formisano: Programmazione Dichiarativa con Prolog, CLP, ASP, e CCP. Available on line (In Italian).

- 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

- Other references are available from the course web site.

Exams

Project and oral discussion on the course program.