Please note! Course description is confirmed for two academic years (1.8.2018-31.7.2020), 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.
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: 09.09.2020 - 14.12.2020
Teacher in charge (valid 01.08.2020-31.07.2022): Tommi Junttila, Jussi Rintanen
Teacher in charge (applies in this implementation): Tommi Junttila, Jussi Rintanen
Contact information for the course (applies in this implementation):
CEFR level (applies in this implementation):
Language of instruction and studies (valid 01.08.2020-31.07.2022):
Teaching language: English
Languages of study attainment: English
CONTENT, ASSESSMENT AND WORKLOAD
Content
Valid 01.08.2020-31.07.2022:
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 01.08.2020-31.07.2022:
Compulsory personal exercises and exam. The overall course grade depends on the points earned from these sources.
Workload
Valid 01.08.2020-31.07.2022:
Lectures, independent work, exercise sessions and examination.
DETAILS
Study Material
Valid 01.08.2020-31.07.2022:
Made available at MyCourses.
Substitutes for Courses
Valid 01.08.2020-31.07.2022:
Replaces courses CS-E3200 Discrete Models and Search, CS-E4540 Answer Set Programming, and CS-E4570 Advanced Course in Boolean Satisfiability.
Prerequisites
Valid 01.08.2020-31.07.2022:
Basics of propositional logic covered, for instance, in the course CS-E4800 Artificial Intelligence. Programming skills in some procedural language such as Python, Java, Scala or C++. Fundamental data structures and algorithms, e.g., the CS-A1140 Data Structures and Algorithms course. Basics on discrete mathematics.
SDG: Sustainable Development Goals
7 Affordable and Clean Energy
9 Industry, Innovation and Infrastructure
FURTHER INFORMATION
- Opettaja: Junttila Tommi
- Opettaja: Rintanen Jussi