 |
| Detailinformationen |
| Quellcurriculum |
Masterstudium Computer Science 2025W |
| Lernergebnisse |
Kompetenzen |
| (*)The students are proficient in recent SAT solving technology.
|
|
| Fertigkeiten |
Kenntnisse |
(*)Students can
- use SAT solvers for solving application problems (K2, K3)
- understand the core algorithms implemented in modern SAT solver (K2, K3, K4)
- implement a simple solver (K5, K6)
- simplify formulas in a satisfiablity preserving manner (K2, K3, K4)
- efficiently transform formulas to conjunctive normal form (K2, K3, K4)
|
(*)- Encoding: NNF, Tseitin, Plaisted-Greenbaum
- Preprocessing: DP, BVE, BVA, blocked clauses, autarkies, probing
- Solving: DPLL, CDCL, learning, implication graph, UIP, clause minimization, clause reduction, incremental solvers.
|
|
| Beurteilungskriterien |
(*)Home exercises and student projects or exam.
|
| Lehrmethoden |
(*)Slide-based lecture, tool demos, small practical projects.
|
| Abhaltungssprache |
Englisch |
| Literatur |
(*)Slides.
Handbook of Satisfiability (Biere, Heule, van Maaren, Walsh).
The Art of Computer Programming Fascile 6a (Knuth)
|
| Lehrinhalte wechselnd? |
Nein |
| Frühere Varianten |
Decken ebenfalls die Anforderungen des Curriculums ab (von - bis)
921CGELAMCK13: KV Advanced Model Checking (2013W-2019S)
|
|
