Module Theory of efficient algorithms, Computer Science (Master) (ER 8)

English language
Compact font

Color scheme

Module summary

Theory of efficient algorithms

INFM210SE

Prof. Dr. Heiko Körner

/

All semesters

none

none

Students will be able to design efficient algorithms in theory and practice. They will be able to prove the correctness of various graph-theoretical problems with exact logical conclusions. They are able to analyse the time complexity of algorithms and use suitable analysis techniques. They will also be able to independently implement modelling and simulation methods for the computer-aided design of process sequences and parallelise various iteration methods on modern high-performance computers.

Written/verbal Exam 120/20 Min. (graded)
Course Graph Algorithms

INFM211SE.a

Lecture

Prof. Dr. Heiko Körner

German

3/2

90 hours in total, including 30 hours of contact study.

Module exam

The course teaches basic algorithms on graphs and shows how to analyse their correctness and time complexity.

After a brief introduction to graph theory, we will first introduce search methods such as breadth-first and depth-first search. Further algorithms deal with the recognition of strongly connected components, topological sorting and finding shortest paths. Efficient tests for the circularity of graphs are also discussed.

The lecture enables participants to independently develop further algorithms, apply them in a provably safe manner and evaluate their usefulness.

  • Discussion at the blackboard
  • Lecture notes
  • Sample solutions for all exercises
  • T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein: Introduction to Algorithms, 4th edition. MIT Press, 2022.

Classical lecture. Several exercises deepen the field of study and are discussed in the classroom if desired.

Course SAT Solving

INFM211SE.a

Lecture

Prof. Dr. Carsten Sinz

German

2/2

60 hours in total, including 30 hours of contact study.

Module exam

SAT solving is one of the most important general methods for solving difficult (often NP-complete) combinatorial problems. These occur in practice in a variety of applications, e.g.:


  • Planning and scheduling problems in supply chains
  • Configuration of complex, multi-variant products, e.g. cars, lorries, aircraft
  • Testing (verification) of hardware and software
  • Creation of match schedules, e.g. soccer leagues


This module teaches students the theoretical and mainly practical aspects of SAT-Solving. It deals with:


  • Fundamentals, historical development
  • Coding, e.g. cardinality constraints
  • Phase transitions in random problems
  • Local search (GSAT, WalkSAT, ..., ProbSAT)
  • Resolution, Davis-Putnam algorithm, DPLL-algorithm, look-ahead algorithm
  • Efficient implementations, data structures
  • Heuristics in the DPLL-algorithm
  • CDCL-algorithm, closed-loop learning, implication graphs
  • Restarts and heuristics in the CDCL-algorithm
  • Preprocessing, inprocessing
  • Generation of proofs and their verification
  • Parallel SAT-Solving (Guiding Paths, Portfolios, Cube-and-Conquer)
  • Advanced applications: Bounded model checking, planning, satisfiability-modulo-theories


Usually industrial users are also integrated.

Course SAT Solving Exercise

INFM212SE

Exercise

Prof. Dr. Carsten Sinz

German

2/1

60 hours in total, including 15 hours of contact study.

Exercise 1 Semester (not graded)

In this exercise, methods of the lecture Practical SAT Solving are tested on the basis of practical problems and SAT-solvers are used to solve combinatorial problems.