Summer Semester 2021
This lecture is about advanced algorithms for SAT solving.
It takes place Wednesdays from 10:15 to 11:45 in Cyberspace trough Zoom starting on March 10.
Recordings of the Zoom sessions will be made available on the moodle page. The current plan is to finish up on June 9.
Grading is based on an oral exam at the end of the course but attendance and taking part in discussions will be taken into account too.
There are plenty of videos referenced on my talks page which cover some part of the lecture usually in a more condensed version but sometimes they also go beyond what is discussed in the lecture.
Version 2019.9 of the slide set is available as satslides.pdf but is usually updated during the semester substantially.
Donald Knuth, The Art of Computer Programming (TAOCP) Volume 4, Fascicle 6: Satisfiability, Addison-Wesley, December 8, 2015 (Volume 4B, Pre-fascicle 6A: A Draft of Section 18.104.22.168: Satisfiability).
You find a description of the Plaisted-Greenbaum polarity based encoding in our recent TACAS paper.