Theory of Combinatorial Algorithms, Institute of Theoretical Computer Science, Department of Computer Science, ETH Zürich

Satisfiablity (SAT) Course, Autumn 2008

Institute of Theoretical Computer Science

Course on

Satisfiability of Boolean Formulas - Combinatorics and Algorithms

Autumn 2008

Overview

Course ID:

German title:

Credits:

more information

Lecturer:

Emo Welzl

Assistant:

Robin Moser

Time:

Location:

Exam:

more information

Language:

Course Contents

Satisfiability (SAT) is the problem of deciding whether a boolean formula in propositional logic has an assignment that evaluates to true. SAT occurs as a problem and is a tool in applications (e.g. Artificial Intelligence and circuit design) and it is considered a fundamental problem in theory, since many problems can be naturally reduced to it and it is the 'mother' of NP-complete problems. Therefore, it is widely investigated and has brought forward a rich body of methods and tools, both in theory and practice (including software packages tackling the problem). This course concentrates on the theoretical aspects of the problem. We will treat basic combinatorial properties (employing the probabilistic method including a variant of the Lovász Local Lemma), recall a proof of the Cook-Levin Theorem of the NP-completeness of SAT, discuss and analyze several deterministic and randomized algorithms and treat the threshold behavior of random formulas. In order to set the methods encountered into a broader context, we will deviate to the more general set-up of constraint satisfaction and to the problem of proper k-coloring of graphs. Primary goals

to study advanced methods in algorithms design and analysis and in discrete mathematics along a classical problem in theoretical computer science
to introduce a number of up-to-date research topics
to provide basis for independent research on the subject (in a semester/diploma/master/doctoral thesis).

Prerequisites

Vordiplomstudium

Literature

Lecture notes

Here is a list of books with material related to the course. They can be found in the textbook collection (Lehrbuchsammlung) of the Computer Science Library:

George Boole, An Investigation of the Laws of Thought on which are Founded the Mathematical Theories of Logic and Probabilities, Dover Publications (1854, reprinted 1973).
Peter Clote, Evangelos Kranakis, Boolean Functions and Computation Models, Texts in Theoretical Computer Science, An EATCS Series, Springer Verlag, Berlin (2002).
Nadia Creignou, Sanjeev Khanna, Madhu Sudhan, Complexity Classifications of Boolean Constrained Satisfaction Problems, SIAM Monographs on Discrete Mathematics and Applications, SIAM (2001).
Harry R. Lewis, Christos H. Papadimitriou, Elements of the Theory of Computation, Prentice Hall (1998).
Rajeev Motwani, Prabhakar Raghavan, Randomized Algorithms, Cambridge University Press, Cambridge, (1995).
Uwe Schöning, Logik für Informatiker, BI-Wissenschaftsverlag (1992).
Uwe Schöning, Algorithmik, Spektrum Akademischer Verlag, Heidelberg, Berlin (2001).
Michael Sipser, Introduction to the Theory of Computation, PWS Publishing Company, Boston (1997).
Klaus Truemper, Design of Logic-based Intelligent Systems, Wiley-Interscience, John Wiley & Sons, Inc., Hoboken (2004).

Course Schedule

Date	Material covered	Exercises
Sep 19	(first lecture) introduction motivating examples (circuit verification, map labelling) conjunctive normal form definition existence of equivalent CNFs polynomial-time conversion into SAT-equivalent CNFs CNF terminology and basic observations introduction to SAT-counting algorithms (to be cont'd)	1.3, 1.5, 1.6, 1.7, 1.9, 1.12, 1.17, 1.18
Sep 26	SAT-counting algorithms (cont'd) resolution soundness completeness extremal properties formulas with few clauses formulas with large clauses formulas with few dependencies among clauses (the Lovász Local Lemma)	1.20, 1.23, 1.28, 2.1, 2.2, 2.6
Oct 3	derandomization of the Local Lemma partial satisfaction (to be cont'd)	2.7, 2.9, 2.1, 2.2, 2.4 (attention: 2.4 is pretty tricky, unless there is a simple way I don't see :)!) Today we've handed out special assignment set 1: download
Oct 10	partial satisfaction (cont'd) algorithms for 2-SAT (to be cont'd)	2.12, 2.15, 3.1, 3.2, 3.3, 3.5
Oct 17	Due date of special assignment set 1! algorithms for 2-SAT (cont'd) a randomized algorithm, analysis using random walks a linear time algorithm	if you haven't looked at them yet, please reconsider last week's exercises, we will discuss them next Friday; additionally, 3.6, 3.11, 3.12, 3.15
Oct 24	applying 2-SAT to graph colouring problems SAT and the Class NP (to be cont'd) verifiers, falsifiers, FP_k - complexity classes	3.17, 3.20, 4.1, 4.5, 4.7 Today we've handed out special assignment set 2: download Attention: this is a corrected version; an additional hypothesis had to be added to Problem 3!
Oct 31	SAT is NP-complete introduction to the Hamming Cube	4.8, 4.9, 4.10, 5.4, 5.5, 5.7
Nov 7	Due date of special assignment set 2! properties of the Hamming cube the volume of Hamming balls	please reconsider last week's exercises, we will discuss them next Friday! Additionally, 5.9, 5.11 Today we've handed out special assignment set 3: download
Nov 14	Hamming cube and Hamming balls Coding and k-SAT algorithms	5.12, 5.13, 5.17, 6.3, 6.4 As usual, these exercises will be discussed in two weeks.
Nov 21	Due date of special assignment set 3! Hamming balls and k-SAT algorithms A randomized algorithm	please reconsider last week's exercises, we will discuss them next Friday! Additionally, 7.1. Today we've handed out special assignment set 4: download
Nov 28	IP=PSPACE (presentation by Robin Künzler) Constraint satisfaction problems	We have handed out 'IP=PSPACE' exercises in class. Apart from that, you might want to look at the CSP exercises 8.1 through 8.3, but there will be no time to discuss these before Dec 12.
Dec 5	Due date of special assignment set 4! Improving the Search Ball Algorithm (by Dominik Scheder) Determining the chromatic number of graphs in time 2^n	The exercises for this week are contained in the material handed out by Dominik.
Dec 12	Random k-CNF Formulas (all of Chapter 9)	(no more exercises, exam takes place next week)
Dec 19	EXAM

Exam and grades

70% final written exam
The exam is open book, i.e. you are allowed to consult any books, handouts and personal notes of your choice. The use of electronic devices is not allowed.
Anybody other than D-INFK students should indicate participation in the exam by email both to Emo Welzl and Robin Moser before (deadline to be announced). D-INFK students are expected to subscribe following official procedures.
Previous exams can be found at [1] through [4] for reference.
30% exercises
At times in the course of term, we will hand out specially marked exercises the solution of which (typeset in LaTeX or similar) is due two weeks later.
Your solutions will be graded, and your three best grades will account for 10% of your final grade each.
You are welcome to discuss these exercises with your colleagues, but we expect you to hand in your own writeup.

Regulations for PhD students

For PhD students the following rule applies for obtaining credit points (KE) for the course. If you successfully solve (grade 4.0 or better) three out of the four special exercises you get a "Testat" and 5 KE. In order to obtain the remaining 3 KE, you have to take and pass the final exam. No credit points are given for simply sitting in the course. Exercises

We will hand out weekly exercises each Friday. You are encouraged to hand in solutions by the following Friday; submitted solutions will be looked at and returned with comments. Note, however, that only the specially marked exercises (see above) will count towards your grade. Nevertheless, we strongly recommend that you solve all weekly problems and attend the exercise classes. What is the "fifth hour" in the Course Catalogue and the eighth credit point supposed to mean?

Apart from three regular lecture (V) hours and one hour of exercises (U), this course comes with one extra fifth hour of independent work (A); so this makes 8 credit points. You will deserve the credits for the A-unit by independent work, i.e. studying and learning material (also prerequisistes) on your own. Details will be announced at the beginning of the course the latest. Lecture Notes

Lecture notes are distributed during the course, including the exercises that we suggest to be worked through. There is no online version of the lecture notes. Errata

where	correction
Extra Chapter 2, Section 2.2, page 4, definition of witness trees	part of the definition was omitted. In the third paragraph, it should read [We demand that a valid witness tree] have more root vertices than glueing vertices and that it [be categorized such that...]
ibid., page 7, algorithm	line 10 (function head is line 0) should read enqueue all of $\Gamma_F(R)$ in Q in lexicographic ordering
ibid.	there is just one symbol named 'Q', all fonts should look the same
Exercise slides of October 10, 2008. Slide 8. "A tight tree count"	the number of such trees should read 1/((d-1)u+1)(du \choose u) instead of 1/(d(u-1)+1)(du choose u). Only then it matches the right hand side, as you can easily verify.