[ 921CGELSASK19 ] KV SAT Solving

Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS M2 - Master's programme 2. 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
Corresponding lecture 921CGELAMCK13: KV Advanced Model Checking (3 ECTS)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment