Schedule: 11.09.2019 - 16.12.2019
Teaching Period (valid 01.08.2018-31.07.2020):
IV-V (Spring 2019), and I-II (Autumn 2019)
Learning Outcomes (valid 01.08.2018-31.07.2020):
Once you have completed the course you have familiarized yourself with the art of declarative programming 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 de-clarative programming paradigm. Moreover, you are aware of the
fundamental algorithmic ideas needed to implement declarative pro-gramming in practice. The hands-on exercises ensure that you will
gain practical modeling skills and substantial familiarity with applica-tion problems and their main characteristics. Whilst you have
acquainted yourself with contemporary solver technology and know how such tools can be readily used to solve problems of interest.
Content (valid 01.08.2018-31.07.2020):
The course covers three main-stream approaches to declarative programming: Boolean satisfiability (SAT), answer set
programming (ASP), and satisfiability modulo theories (SMT). Select-ed topics depending on the paradigm of interest such as efficient logical representations in terms of formulas and rules, normal forms, contemporary (conflict-driven, learning) algorithms for the search of
satisfying assignments that correspond to solutions of problems. Translation of logical knowledge into normal forms and other logical
representations. The realization of various reasoning tasks through satisfiability and/or by exploiting normal forms, e.g., query
answering, equivalence checking, counting solutions, and finding optimal solutions. Identifying essential properties when modeling
various kinds of problems and systems with logic.
Details on the course content (applies in this implementation):
Constraint programming and satisfiability testing have in the last two decades emerged as an important framework for solving computationally difficult problems in software engineering and design automation (HW, SW).
The course is an introduction to the foundations of declarative programming and its applications. Topics covered include leading algorithms for satisfiability testing and constraint satisfaction, numeric constraint satisfaction, symbolic data structures such as Binary Decision Diagrams (BDD), symbolic reachability analysis methods, temporal logic model-checking, and SAT modulo Theories (SMT).
Assessment Methods and Criteria (valid 01.08.2018-31.07.2020):
Compulsory programming assignments, tutorial exercises, and exam. The overall course grade depends on the points earned from these sources.
Workload (valid 01.08.2018-31.07.2020):
Lecturesh, exercise sessions, independent work, and examination.
Study Material (valid 01.08.2018-31.07.2020):
Made available at MyCourses.
Substitutes for Courses (valid 01.08.2018-31.07.2020):
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.2018-31.07.2020):
Basics of propositional logic covered, e.g., by 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.
Grading Scale (valid 01.08.2018-31.07.2020):
- Teacher: Saurabh Fadnis
- Teacher: Tommi Junttila
- Teacher: Jussi Rintanen