Inhalt

[ 921CGELSASK19 ] KV SAT Solving

Versionsauswahl
Es ist eine neuere Version 2023W dieser LV im Curriculum Masterstudium Computational Mathematics 2023W vorhanden.
Workload Ausbildungslevel Studienfachbereich VerantwortlicheR Semesterstunden Anbietende Uni
3 ECTS M2 - Master 2. Jahr Informatik Armin Biere 2 SSt Johannes Kepler Universität Linz
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)
Präsenzlehrveranstaltung
Teilungsziffer -
Zuteilungsverfahren Direktzuteilung