6 ECTS credits
168 h study time

Offer 1 with catalog number 4022171FNR for all students in the 1st semester at a (F) Master - specialised level.

Semester
1st semester
Enrollment based on exam contract
Impossible
Grading method
Grading (scale from 0 to 20)
Can retake in second session
Yes
Taught in
English
Faculty
Faculty of Sciences and Bioengineering Sciences
Department
Computer Science
Educational team
Bart Bogaerts (course titular)
Activities and contact hours
26 contact hours Lecture
26 contact hours Seminar, Exercises or Practicals
Course Content


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. 

Additional info


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

Learning Outcomes

Algemene competenties


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.
 
 

Grading

The final grade is composed based on the following categories:
Other Exam determines 100% of the final mark.

Within the Other Exam category, the following assignments need to be completed:

  • Other Exam with a relative weight of 1 which comprises 100% of the final mark.

Additional info regarding evaluation


The evaluation consists of three parts:

Project work: 40%
Presentation(s) during classes: 20%
Oral Exam: 40%

Allowed unsatisfactory mark
The supplementary Teaching and Examination Regulations of your faculty stipulate whether an allowed unsatisfactory mark for this programme unit is permitted.

Academic context

This offer is part of the following study plans:
Master of Applied Sciences and Engineering: Computer Science: Artificial Intelligence
Master of Applied Sciences and Engineering: Computer Science: Multimedia
Master of Applied Sciences and Engineering: Computer Science: Software Languages and Software Engineering
Master of Applied Sciences and Engineering: Computer Science: Data Management and Analytics