Module Theory of efficient algorithms, Computer Science (Master) (ER 8)
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.
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.
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.
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.