[ 921CGELSASK19 ] KV SAT Solving

Es ist eine neuere Version 2023W dieser LV im Curriculum Master's programme Computational Mathematics 2023W vorhanden.
Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS M1 - Master's programme 1. year Computer Science Martina Seidl 2 hpw Johannes Kepler University Linz
Detailed information
Original study plan Master's programme Computer Science 2021W
Objectives The students are proficient in recent SAT solving algorithms.
  • 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.
Criteria for evaluation Oral exam, student projects.
Methods Slide-based lecture, tool demos, small practical projects.
Language English
Study material Slides. Handbook of Satisfiability (Biere, Heule, van Maaren, Walsh). The Art of Computer Programming Fascile 6a (Knuth)
Changing subject? No
Further information

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

Earlier variants They also cover the requirements of the curriculum (from - to)
921CGELAMCK13: KV Advanced Model Checking (2013W-2019S)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment