6 ECTS credits
168 u studietijd
Aanbieding 1 met studiegidsnummer 4022171FNR voor alle studenten in het 1e semester met een gespecialiseerd master niveau.
This is a research oriented course in which we study fundamentals principles of modern declarative problem solving techniques. We start from SAT solving, which lies at the basis of many modern combinatorial search solvers from various domains, and study strengths and weaknesses of modern SAT solvers, and the algorithms on which they are built.
Later in the course, we turn our attention to more expressive, higher level modelling paradigms (such as Answer Set Programming and Constraint Programming) and study their relation with SAT, in particular, lazy and eager reductions.
The course material consists of research papers and slides on the topic and will be announced on Canvas.
Topics that will be handled:
Part 1: SAT:
- Introduction to SAT solving and conflict drive clause learning
- Using SAT Oracles (MaxSAT - core-guided, hitting-set; generating unsatisfiable subsets; (QBF))
- Proof Logging (RUP, RAT, DRAT)
- Symmetry in SAT
Part 2: Modelling Languages
- Minizinc
- Answer Set Programming
Part 3: Relating High-level Languages with Low-Level Solvers
- Grounding techniques in ASP
- Lazy Clause Generation (in CP and ASP)
- Lazy Grounding Methods
Part 4: Exotic topics.
- Topics handled in this part will vary each year
The goals of this course are:
Students obtain knowledge about modern search techniques
Students become skilled in modeling a problem domain in a suitable declarative problem solving paradigm
Students can independently process modern research papers on declarative search methods.
The corresponding learning results are:
w.r.t. knowledge:
The student knows the basic principles of knowledge representation and reasoning and knows (characterizations of) the stable semantics of logic programs. They know the working of modern search techniques for SAT, ASP, and constraint solving, including conflict-driven clause learning, unfounded set propagation, lazy grounding, and lazy clause generation.
w.r.t. applying knowledge:
The student can model a given problem in a given vocabulary and optimize their model in towards performance of the underlying system. The student can transfer modern search techniques to fields beyond what is studied in this course.
w.r.t. analyzing
The student can analyze a problem domain and critically evaluate whether the problems arising in the domain in question can be tackled using ASP, SAT or Constraint Programming. If yes, they can devise a suitable vocabulary.
The student can independently process a scientific research paper on the topic of declarative problem solving: summarize it and report verbally on it.
w.r.t. evaluating
The student can analyze strengths and weaknesses of novel search techniques and declarative problem solving techniques.
w.r.t. creating
The student can create declarative models of a given problem domain.
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:
The evaluation consists of three parts:
Project work: 40%
Presentation(s) during classes: 20%
Oral Exam: 40%
Deze aanbieding maakt deel uit van de volgende studieplannen:
Master in Applied Sciences and Engineering: Computer Science: Artificial Intelligence (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Multimedia (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Software Languages and Software Engineering (enkel aangeboden in het Engels)
Master in Applied Sciences and Engineering: Computer Science: Data Management and Analytics (enkel aangeboden in het Engels)