Course on

Satisfiability of Boolean Formulas - Combinatorics and Algorithms

(37-491 Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen, 2V1U, 5 credits)
Emo Welzl (lecturer) and Robert Berke (assistant)
Winter 2004/05, Friday, 10-12 (IFW B42, lectures) and 13-14 (IFW B42, exercises)
Language: English (German, in case nobody expresses preference for English)

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.

Goal. Introduction to(wards) a number of up-to-date research topics. Provide basis for independent research on the subject (in a semester/Diplom/master/doctoral thesis).

Prerequisites. The course assumes basic knowledge in propositional logic, probability theory and discrete mathematics, as it is supplied in the Vordiplomstudium.

Literature. There exists no book that covers the many facets of the topic. Lecture notes covering the material of the course will be distributed (Errata, updates, see below).

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).

---

A Course Schedule.
[22 Okt] (for an exception, lectures extend to the exercises in the afternoon.)
Material covered: Introduction, examples (circuit verification, map labeling), conjunctive normal form, terminology, 3hrs.
Exercises "handed out": 1.3, 1.6, 1.12, 1.17, 1.18.
[29 Okt] Material covered: Counting satisfying assignments, resolution.
Exercises "handed out": 1.20, 1.21, 1.25, 1.29.
[5 Nov] Material covered: Extremal properties (number of clauses/of dependent clauses).
Exercises "handed out": 2.1, 2.2, 2.4.
[12 Nov] Material covered: Partial satisfaction, 2-SAT (resolution, unit clause reduction).
Exercises "handed out": 2.9, 2.10, 2.18, 3.3.
[19 Nov] Material covered: 2-SAT (random walk, implication graph).
Exercises "handed out": 3.6, 3.11, 3.12, 3.13.
[26 Nov] Material covered: 2-SAT applications, SAT and NP (coloring vs SAT).
Exercises "handed out": 3.17, 3.18, 3.20, 4.2.
[3 Dec] Material covered: SAT and NP (polynomial verifiers and k-falsifiers, class NP and relatives FPk).
Exercises "handed out": 4.4, 4.5, 4.6.
[10 Dec] Material covered: SAT and NP (polynomial reductions, SAT is NP-complete).
Exercises "handed out": 2.3, 3.19, 4.9.
[17 Dec] Material covered: The cube (faces, packing and covering, Kraft Inequality, degree condition for induced subgraphs of cubes, volume of Hamming balls, existence of small covering codes).
Exercises "handed out": 5.1, 5.4, 5.6, 5.9, 5.10, 5.12, 5.14, 5.17.
---(X-mas break)---
[14 Jan] Material covered: 3 hours discussion of exercises (and other material on request).
Exercises "handed out": .
[21 Jan] (lectures extend to the exercises into the afternoon)
Material covered: Satisfiability Coding Lemma, Paturi-Pudlák-Zane algorithm (randomized).
Exercises "handed out": .
[28 Jan] (lectures extend to the exercises into the afternoon)
Material covered: Deterministic k-SAT algorithm (Hamming ball search, construction of small covering codes), Schöning algorithm (local random walk search).
Exercises "handed out": .
[4 Feb] Material covered: Constraint satisfaction
---(end of semester)---
[Monday 28 Feb, 14:00-16:00 @ RZ F21] Exam: Check out last year's exam (SATexamFeb04.pdf or SATexamFeb04.ps). For further information see below.

---

Lecture Notes. Lecture notes are distributed during the course, including the exercises that we suggest to work through. There is no on-line accessible version of the lecture notes.

Link to Updates

Errata:

• Page 69, Exercise 4.2: The idea cannot be used, at least not in the (an) obvious way, for reproving Lemma 4.1. It can be used for constant k, though (so, for example, for Proper 3-Coloring).
• page 72, line +12: F rejects <w,c_S,S> for all S ... --> F rejects <w,c_S,S> for some S ... (thanks to Roland Lötscher)
• page 87, line +7: ... maps an even number of ... --> ... maps an odd number of ...
• page 91, line +11, item (v): "for r in Z" should be added
• page 96: h(rho) should be H(rho)

---

Exam: There is a written 2 hours exam that takes place February 28, 2005 from 14:00 to 16:00 at room RZ F21 , also for the students from D-MATH. You are allowed to take any kind of written material with you, but no electronic devices of whatever kind.
Anybody other than D-INFK students should indicate participation in the exam by email both to Emo Welzl and Robert Berke on January 27, 2005 or before. (D-INFK students are assumed to have subscribed for the exam through the usual procedures.)

Material relevant for the exam is as given in the lecture notes handed out, Chapters 1 through 8 and Glossary of Notions and Facts, with the only exception of the symmetrization proof of Theorem 2.5, but with its proof given in Note 2.5 instead. Note that Chapter 9 which was handed out is not required for the exam.

---