Lecture Notes

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 SAT-solvers, which are often able to solve large instances that occur in practical applications. Practical SAT-solvers are based on heuristics, in the sense that they either don't have provable correctness guarantees, or they don't have good worst-case 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 3-CNF 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


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