Lecture Notes
 Oct 23: Randomized local search for 3CNFSAT
 Oct 30: Deterministic local search for 3CNFSAT
 Nov 13: Guess & Conquer: The bestknown algorithm for kCNFSAT
 Nov 20: Analysis of Guess & Conquer
 Nov 25: The bestknown algorithm for general CNFSAT
 Nov 27: Algorithms for Quantified Boolean CNF Formulas
 Dec 4: The switching lemma
 Dec 9: An algorithm for AC0SAT
 Jan 15: The sparsification lemma
 Jan 20: The sparsification lemma II
 Jan 29: The isolation lemma
 Feb 3: Sparsification lower bounds
 Feb 27: An algorithm for ACCSAT
 Mar 2: ACC circuit lower bounds
Description
The satisfiability problem is the problem of deciding whether a given Boolean circuit has a satisfying assignment. It is a fundamental problem in computer science that captures a plethora of questions, including but not limited to questions arising in artificial intelligence, chip design, and verification. Due to the problem’s importance, research and engineering teams around the world have produced and optimized SATsolvers, which are often able to solve large instances that occur in practical applications. Practical SATsolvers are based on heuristics, in the sense that they either don’t have provable correctness guarantees, or they don’t have good worstcase running times.
In this course, we will explore recent theoretical progress on provably correct algorithms that solve the satisfiability problem for various restricted classes of Boolean circuits, such as 3CNF formulas, CNF formulas, and ACC circuits. Depending on the interest and background of the participants, we may also discuss negative results that try to rule out faster algorithms for satisfiability, results that transfer the complexity of satisfiability to other problems and contexts, and we may discuss the implications that faster algorithms have for complexity theory’s holy grail: circuit lower bounds.
Workload and Grading
Every couple of weeks, you will get a homework assignment designed to enhance your comprehension of the material. Apart from standard assignments, I may ask you to read research articles, write short essays about them, or present them to your classmates and to your instructor either in class or in the occasional tutorial session. You will receive a ‘pass’, ‘fail’, or ‘excellent’ for each homework; two fails mean that you fail the class.
There will be an oral exam at the end of the semester which will determine your overall grade for the course. Each homework that was rated ‘excellent’ will boost your final grade by 1/3, but the total boost cannot exceed 1. For example, if you get a 2.0 in the oral exam and you handed in two excellent homeworks, then your grade will be 1.3. If you are eligible to take the oral exam and fail, you can take the oral exam a second time.
The course will give 5 ETCS.
Prerequisites
We will develop the material pretty much from scratch, but we will do so quickly. Thus you should already be familiar with algorithms, discrete mathematics (graphs etc.), and some linear algebra. Experience in randomized algorithms, theoretical computer science, and complexity theory are helpful, but not required.
References

Algorithmica 2002 / FOCS 1999

Chicago Journal of Theoretical Computer Science 1999 / FOCS 1997

STACS 2011

SIAM Journal on Computing 2014 / FOCS 2011

SAT 2005

SODA 2012

SODA 2015

JCSS 2008

IWPEC 2008

ICALP 2014

CCC 2006

SODA 2010

SODA 2015

STOC 2014

SODA 2002
Despite the metal and wires, I still have human desires.*