Please note! Course description is confirmed for two academic years, which means that in general, e.g. Learning outcomes, assessment methods and key content stays unchanged. However, via course syllabus, it is possible to specify or change the course execution in each realization of the course, such as how the contact sessions are organized, assessment methods weighted or materials used.


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: 07.09.2022 - 12.12.2022

Teacher in charge (valid for whole curriculum period):

Teacher in charge (applies in this implementation): Tommi Junttila, Jussi Rintanen

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


  • 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.

  • valid for whole curriculum period:

    Lectures, independent work, exercise sessions and examination.


Substitutes for Courses
SDG: Sustainable Development Goals

    7 Affordable and Clean Energy

    9 Industry, Innovation and Infrastructure


Further Information
  • valid for whole curriculum period:

    Teaching Language : English

    Teaching Period : 2022-2023 Autumn I - II
    2023-2024 Autumn I - II