Edward A. Hirsch
: Course:
Boolean Satisfiability
This is a 2023 version of the course. Check the main webpage for newer versions.
Lecture notes (Winter 2023/24):
Lecture 1: Introduction
.
Lecture 2: Faster-than-2
n
algorithms (Part I)
.
Lecture 3: Faster-than-2
n
algorithms (Part II)
.
Lecture 4: The Exponential Time Hypothesis
.
Lecture 5: The Resolution proof system
.
Lecture 6: Conflict-driven clause learning
.
Lecture 7: Exponential size lower bounds for Resolution
.
Lecture 8: Cutting Planes and other proof systems
.
Lecture 9: Frege and Extended Frege systems.
Lecture 10: Exponential-size lower bounds for Cutting Planes. Short proofs of PHP in Frege systems.