|
Detailinformationen |
Quellcurriculum |
Masterstudium Computer Science 2021S |
Ziele |
Command of 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.
|
Lehrmethoden |
Lecture, slides.
|
Abhaltungssprache |
Englisch |
Literatur |
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
|
Äquivalenzen |
921CGELAMCK13: KV Advanced Model Checking (3 ECTS)
|
Frühere Varianten |
Decken ebenfalls die Anforderungen des Curriculums ab (von - bis) 921CGELAMCK13: KV Advanced Model Checking (2013W-2019S)
|
|