 |
| Detailinformationen |
| Quellcurriculum |
Masterstudium Computer Science 2023W |
| Ziele |
(*)The students are proficient in recent SAT solving algorithms.
|
| Lehrinhalte |
(*)- Encoding: NNF, Tseitin, AIGs, cardinality constrains encoding, bit-blasting.
- Preprocessing: DP, BVE, BVA, blocked clauses, autarkies, Stalmarck, Recursive Learning, clause redundancy, probing.
- Solving: DPLL, CDCL, learning, implication graph, failed literals, UIP, clause minimization, restarts, clause reduction.
|
| Beurteilungskriterien |
(*)Oral exam, student projects.
|
| 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 |
| Sonstige Informationen |
(*)http://fmv.jku.at/sat
|
| Frühere Varianten |
Decken ebenfalls die Anforderungen des Curriculums ab (von - bis)
921CGELAMCK13: KV Advanced Model Checking (2013W-2019S)
|
|
