DM850: Satisfiability (10 ECTS)

STADS: 15018401

Level
Master's level course approved as PhD course

Teaching period
The course is offered in the spring semester.

Teacher responsible
Email: petersk@imada.sdu.dk

Timetable
Show entire timetable
Show personal time table for this course.

Comment:
Ubegrænset deltagerantal.

Prerequisites:
A bachelor degree in computer science, mathematics, applied mathematics, mathematics-economy or comparable.

Academic preconditions:
Students following the course are expected to:

• have knowledge of basic terms and concepts regarding propositional logic and first order logic.
• be able to apply basic transformations of logical expressions as well as reason about the truth of logic formulas.
• be able to judge the complexity of algorithms, with regard to runtime as well as with regard to space usage.

Course introduction
The purpose of the course is to enable the student to apply Satisfiability as a method in order to solve computationally non-trivial problems in a nevertheless often practically efficient way. Translating problems to Satisfiability (both SAT and SMT) has become a standard method in many areas of computer science, all the way from model checking to bioinformatics, such that knowledge of and proficiency in Satisfiability are relevant for a master of computer science.

The course builds on the knowledge gained in the courses DM549 Discrete Methods for Computer Science and DM552 Programming Languages. Likewise concepts from DM554 Complexity and Computability and DM554 Linear and Integer Programming can be applied to the course. The course provides a basis for a master thesis, in which SAT or SMT is applied.

In relation to the learning outcomes of the degree the course has explicit focus on:

• giving the competence to plan and execute scientific projects of high standard on the background of projects based on scientific articles/book chapters.
• developing skills in the development of new variants of the learned methods, where the concrete problem requires it on the background of the high bandwidth of subjects covered by the scientific articles/book chapters.
• developing skills in the dissemination of research-based knowledge and discussion of professional and scientific problems on the background of student-run seminars.
• providing knowledge on a selection of specialized models and methods developed in computer science based on the highest level of international research, including subjects from the research front on the background of the selection of the scientific articles/book chapters.
• providing knowledge about computer science models and methods meant for application to other subjects on the background of the high bandwidth of subjects covered by the scientific articles/book chapters.
• provide expert knowledge of a selected area of study, based on the highest level of international research within the field of computer science on the background of the teachers active role in the research field.

Expected learning outcome
To reach the purpose of the course, the student is expected to demonstrate the ability to:

• demonstrate foundational knowledge of the principles and algorithms behind SAT and SMT solvers. 
• judge whether a translation to SAT or SMT is a relevant method for solving a given problem.
• understand and consequently disseminate both in written form and orally scientific articles/book chapters from the research area.
• apply and transfer methods from the presented applications to new problems, also in the context of other subjects.
• implement solutions based on a translation to SAT or SMT and apply state-of-the-art SAT or SMT solvers to the result.

Subject overview
The course contains the following main areas:

• the SAT problem and trivial SAT solvers
• the DPLL algorithm and other indispensable components of state-of-the-art SAT solvers
• the SMT problem and associated theories
• the DPLL(T) algorithm and examples of concrete instances 
• principles for effective translations to SAT
• coding methods for different standard constructions
• application of SAT and SMT solvers to problems from different areas

Literature

Meddeles ved kursets start.

Website
This course uses e-learn (blackboard).

Prerequisites for participating in the exam
Oral presentation. Pass/fail, internal evaluation by teacher.

Assessment and marking:
Project assignment. Evaluated by Danish 7-mark scale, external censorship.

Expected working hours
The teaching method is based on three phase model.
Intro phase: 28 hours
Skills training phase: 28 hours, hereof:
 - Tutorials: 14 hours
 - Laboratory exercises: 14 hours

Educational activities

Educational form
The teaching in the introduction phaseis partitioned into two parts. The first part consists of interactive lectures covering the relevant principles. The second part consits of seminar-style teaching, where the students present and discuss on the background of assigned scientific articles/book chapters regarding different applications.

The training phase is partitioned into discussion sections, where the material and in particular the scientific articles/book chapters are discussed, and lab exercises, where practical skills in the application of relevant tools are practised.

Furthermore, the acquired knowledge is applied in projects, which are elaborated in the study phase. The scientific sources, which were the foundation of the seminar part, and the project are summarized in a scientific manuscript.

Language
This course is taught in Danish or English, depending on the lecturer. However, if international students participate, the teaching language will always be English.

Course enrollment
See deadline of enrolment.

Tuition fees for single courses
See fees for single courses.