[ 921CGELSASK19 ] KV SAT Solving

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 2023W
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
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