Tidtabel: 11.09.2019 - 16.12.2019
Undervisningsperiod (är i kraft 01.08.2018-31.07.2020):
IV-V (Spring 2019), and I-II (Autumn 2019)
Lärandemål (är i kraft 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.
Innehåll (är i kraft 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.
Närmare beskrivning av kursens innehåll (gäller denna kursomgång):
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).
Metoder, arbetssätt och bedömningsgrunder (är i kraft 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.
Arbetsmängd (är i kraft 01.08.2018-31.07.2020):
Lecturesh, exercise sessions, independent work, and examination.
Studiematerial (är i kraft 01.08.2018-31.07.2020):
Made available at MyCourses.
Ersättande prestationer (är i kraft 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.
Förkunskaper (är i kraft 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.
Bedömningsskala (är i kraft 01.08.2018-31.07.2020):