[ 921CGELSASK19 ] KV SAT Solving

Es ist eine neuere Version 2021W dieser LV im Curriculum Master's programme Computer Mathematics 2021W vorhanden.
(*) Unfortunately this information is not available in english.
Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS M2 - Master's programme 2. year Computer Science Armin Biere 2 hpw Johannes Kepler University Linz
Detailed information
Original study plan Master's programme Computer Science 2021S
Objectives Command of SAT solving algorithms
Subject 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.
Methods Lecture, slides.
Language English
Study material 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