Inhalt

[ 921CGELSASK19 ] KV (*)SAT Solving

Versionsauswahl
Es ist eine neuere Version 2023W dieser LV im Curriculum Masterstudium Computational Mathematics 2023W vorhanden.
(*) Leider ist diese Information in Deutsch nicht verfügbar.
Workload Ausbildungslevel Studienfachbereich VerantwortlicheR Semesterstunden Anbietende Uni
3 ECTS M1 - Master 1. Jahr Informatik Martina Seidl 2 SSt Johannes Kepler Universität Linz
Detailinformationen
Quellcurriculum Masterstudium Computer Science 2021W
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

Until term 2019S known as: 921CGELAMCK13 KV Advanced Model Checking

Frühere Varianten Decken ebenfalls die Anforderungen des Curriculums ab (von - bis)
921CGELAMCK13: KV Advanced Model Checking (2013W-2019S)
Präsenzlehrveranstaltung
Teilungsziffer -
Zuteilungsverfahren Direktzuteilung