(This course was previously taught in 2023/24: the previous version is kept here for further reference.)

Lecture notes (Spring 2026):

• Lecture 1: Introduction. Schaefer's Dichotomy Classification.
• Lecture 2: Faster-than-2ⁿ algorithms (Part I: DPLL, randomized PPZ).
• Lecture 3: Faster-than-2ⁿ algorithms (Part II: deterministic PPZ, randomized and deterministic local search and random walk, solving SAT beyond k-SAT).
• Lecture 4: The Exponential Time Hypothesis (ETH) and Strong ETH (SETH).
• Lecture 5: The Resolution proof system, its treelike version that is equivalent to decision trees and DPLL.
• Lecture 6: Conflict-driven clause learning: CDCL SAT Solvers.
• Lecture 7: Proof systems (formally). Exponential size lower bounds for Resolution.
• (To be continued.)