[  news | contents | resources ]

SAT Solving

Summer Semester 2021

Armin Biere

News

New web-page.

Contents

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.

Resources

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 7.2.2.2: Satisfiability).

You find a description of the Plaisted-Greenbaum polarity based encoding in our recent TACAS paper.

As background material consider the Handbook of Satisfiability (see also the tutorial page of the SAT association). The 2nd edition is about to be published soon (see also http://tiny.cc/SAT2021).

The SAT Association, the SAT conference, and the SAT Competition.

Further related papers are listed on our publication page, additional software, particularly SAT solvers, can be found on our software page