6 ECTS credits
168 u studietijd
Aanbieding 1 met studiegidsnummer 4022170FNR voor alle studenten in het 1e semester met een gespecialiseerd master niveau.
Dit is een research-gericht vak waarin we fundamentele principes onderliggend aan moderne declaratieve probleemoplossers bestuderen.
We beginnen dit vak met SAT solving, hetgeen aan de basis ligt van heel wat hedendaagse oplossers van combinatorische problemen uit verschillende domeinen, en we bestuderen sterktes en limitaties van moderne SAT solvers, en de algoritmes waarop deze gebouwd zijn.
Later in het vak richten we onze aandacht op meer expressieve hoogniveau modelleerparadigmas (zoals Answer Set Programming en Constraint Programming) en bestuderen hun relatie met SAT, in het bijzonder luie en gretige reducties naar SAT.
Het cursusmateriaal bestaat voornamelijk uit onderzoekspapers en slides over de behandelde onderwerpen en wordt op Canvas bekendgemaakt.
Onderwerpen die behandeld zullen worden:
Deel 1: SAT:
- Introductie tot SAT solving en conflict drive clause learning
- Het gebruiken van SAT orakels (MaxSAT - core-guided, hitting-set; zoeken van onvervulbare deelverzamelingen; (QBF))
- Loggen van bewijzen (RUP, RAT, DRAT)
- Symmetrie in SAT
Deel 2: Modelleertalen
- Minizinc
- Answer Set Programming
Deel 3: Het verband tussen hoogniveau talen en laagniveau oplossers
- Grounding technieken in ASP
- Lazy Clause Generation (in CP and ASP)
- Methodes voor Lui Grounden
Part 4: Exotische onderwerpen.
- De onderwerpen in dit deel zullen elk jaar variëren.
De doelen van dit vak zijn:
Studenten verweren kennis van moderne zoekalgoritmes
Studenten zijn bekwaam in het modelleren van probleemdomeinen in een gepast declaratief probleemoplossingsparadigma.
Studenten kunnen onafhankelijk moderne onderzoekspapers over declaratieve oplossingsmethodes verwerken.
De overeenkomstige leerresultaten zijn:
m.b.t. kennis:
De student kent de basisprincipes van kennisrepresentatie en redeneren en kent (karakterisaties) van de stable semantics van logische programmas. Hij/zij kent de werking van moderne zoekstrategieën voor SAT, ASP en constraint solving, zoals conflict-driven clause learning, unfounded set propagatie, lazy grounding en lazy clause generation.
m.b.t. toepassen van kennis:
De student kan een gegeven probleem modelleren in een gegeven vocabularium en zijn/haar model optimaliseren naar perfomantie van het gebruikte systeem. De student kan moderne zoektechnieken toepassen op domeinen buiten degene bestudeerd in deze cursus.
m.b.t. analyseren
De student kan een probleemdomein analyseren en kritisch evalueren of de problemen die in het domein opduiken kunnen opgelost worden met ASP, SAT of constraint programming. Indien ja, kunnen ze een gepast vocabularium hiervoor ontwerpen.
De student kan onafhankelijk een onderzoekspaper over het onderwerp van declaratief probleemoplossen verwerken, deze samenvatten en hier verbaal over communiceren.
m.b.t. evalueren
De student kan sterktes en zwaktes van nieuwe zoekalgoritmes en declaratieve oplossingsmethodes beoordelen.
m.b.t. creëren
De student kan declaratieve modellen van een gegeven probleemdomein ontwerpen
De beoordeling bestaat uit volgende opdrachtcategorieën:
Examen Andere bepaalt 100% van het eindcijfer
Binnen de categorie Examen Andere dient men volgende opdrachten af te werken:
De evaluatie bestaat uit drie delen
Projectwerk: 40%
Presentatie(s) tijdens de lessen: 20%
Mondeling examen: 40%
Deze aanbieding maakt deel uit van de volgende studieplannen:
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Artificiële Intelligentie
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Multimedia
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Software Languages and Software Engineering
Master in de ingenieurswetenschappen: computerwetenschappen: afstudeerrichting Data Management en Analytics