 |
| Detailed information |
| Original study plan |
Master's programme Computer Science 2021W |
| Objectives |
The students are proficient in recent 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, 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 |
http://fmv.jku.at/sat
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)
|
|
