Modul

See partial achivement.

Students are able to evaluate combinatorial problems, assess their complexity, and solve them using computers.

Students learn how to solve combinatorial problems efficiently using SAT Solving. Students are able to assess the practical complexity of decision and optimization problems, encode problems as SAT problems, and implement efficient solution procedures for combinatorial problems.

Students gain insight into state-of-the-art solution methods for SAT and related problems and their implementations in SAT solvers.

See partial achivement.

The problem of propositional satisfiability (SAT) is an outstanding problem of computer science from a theoretical as well as practical perspective. Being the first problem proven to be NP-complete, it serves as a fundamental tool for research in complexity theory. Moreover, SAT solving has been established as one of the most important fundamental methods in hardware and software verification, and is used to solve hard combinatorial problems in industrial practice as well. This module aims to provide students with the theoretical and practical aspects of SAT-Solving. Covered are:
1. basics, historical development
2. encodings, e.g. cardinality constraints
3. phase transitions in random problems
4. local search (GSAT, WalkSAT, ..., ProbSAT)
5. resolution, Davis-Putnam algorithm, DPLL algorithm, look-ahead algorithm
6. efficient implementations, data structures
7. heuristics in the DPLL algorithm
8. CDCL algorithm, clause learning, implication graphs
9. restarts and heuristics in the CDCL algorithm
10. preprocessing, inprocessing
11. generation of proofs and their checking
12. parallel SAT solving (guiding paths, portfolios, cube-and-conquer)
13. related problems: MaxSAT, MUS, #SAT, QBF
14. advanced applications: Bounded model checking, planning, satisfiability-modulo-theories

Lecture (2 SWS) + exercise (1 SWS)

(Preparation and follow-up: 4h/week, exercises: 2h/week, preparation for exam: 15h)

Total workload: (2 SWS + 1 SWS + 4 SWS + 2 SWS) x 15 h + 15h preparation = 9x15h + 15h = 150h = 5 ECTS