LEARNING OUTCOMES
Once you have completed the course you have familiarized yourself with the art of declarative programming with constraint solvers, where the goal is to specify what is to be computed rather than how the actual computation is to take place. You will have an in-depth understanding of central logical representations deployed in the paradigm. Moreover, you are aware of the fundamental algorithmic ideas needed to implement constraint solver tools in practice. You will have a good understanding of some of the main applications of declarative and model-based solution methods, including analysis of discrete systems by state-space search. The hands-on exercises ensure that you will gain practical modeling skills and substantial familiarity with application problems and their main characteristics.
Credits: 5
Schedule: 15.09.2021 - 20.12.2021
Teacher in charge (valid for whole curriculum period):
Teacher in charge (applies in this implementation): Jussi Rintanen, Tommi Junttila
Contact information for the course (applies in this implementation):
CEFR level (valid for whole curriculum period):
Language of instruction and studies (applies in this implementation):
Teaching language: English. Languages of study attainment: English
CONTENT, ASSESSMENT AND WORKLOAD
Content
valid for whole curriculum period:
The course covers selected mainstream approaches to declarative programming with constraint solvers, such as Boolean satisfiability (SAT), constraint satisfaction problems (CSP) and satisfiability modulo theories (SMT), as well as some of their most important applications in computer-aided verification and validation of software and hardware systems.
In addition to some of the algorithmic technologies for constraint programming, the course acts as an introduction to declarative and model-based solution of hard computational problems. Application problems are solved by first representing the problem declaratively (as opposed to procedurally) in a high-level modeling language, and then finding one or more solutions by using a general-purpose solver for the high-level modeling language. The declarative models have a semantics separate from the solver algorithms, and the models can be used for multiple purposes and with different types of solver technologies. For example, the same model could be used for control and decision-making, diagnosis, and monitoring.
Specific contents are given on the MyCourses page of the course instance.
Assessment Methods and Criteria
valid for whole curriculum period:
Compulsory personal exercises and exam. The overall course grade depends on the points earned from these sources.
Workload
valid for whole curriculum period:
Lectures, independent work, exercise sessions and examination.
DETAILS
Study Material
valid for whole curriculum period:
Made available at MyCourses.
Substitutes for Courses
valid for whole curriculum period:
Prerequisites
valid for whole curriculum period:
SDG: Sustainable Development Goals
7 Affordable and Clean Energy
9 Industry, Innovation and Infrastructure
FURTHER INFORMATION
Further Information
valid for whole curriculum period:
Teaching Period:
2020-2021 Autumn I-II
2021-2022 Autumn I-II
Course Homepage: https://mycourses.aalto.fi/course/search.php?search=CS-E3220
Registration for Courses: In the academic year 2021-2022, registration for courses will take place on Sisu (sisu.aalto.fi) instead of WebOodi.