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 Milos Stojakovic (assistant)
Winter 2003, Friday, 10-12 (IFW B42, lectures) and 13-14 (IFW B42, exercises)
Language: 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 (it is complementary to the SAT part of the parallel course Formal Verification by Armin Biere with emphasis on practical issues including tools and applications). 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, briefly treat the threshold behavior of random formulas, and consider approximation algorithms and inapproximability results for the MAX-SAT problem (of satisfying as many clauses as possible in a formula in conjunctive normal form).
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.

---

A Course Schedule.
[24 Okt] Material covered: Introduction, examples (circuit verification, map labeling), conjunctive normal form, terminology, 3hrs.
Exercises "handed out": 1.3, 1.4, 1.12, 1.17, 1.18, 1.19.
[31 Okt] Material covered: Counting satisfying assignments, resolution.
Exercises "handed out": 1.20, 1.25, 1.29.
[7 Nov] Material covered: Extremal properties (number of clauses/of dependent clauses).
Exercises "handed out": 2.1, 2.3, 2.6.
[14 Nov] Material covered: 3 Hrs exercise discussion, no lectures.
Exercises "handed out": -
[21 Nov] Material covered: Partial satisfaction, 2-SAT (resolution, unit clause reduction), 3hrs.
Exercises "handed out": 2.17, 3.1, 3.3, 3.4, 3.6.
[28 Nov] Material covered: 2-SAT (random walk, implication graph).
Exercises "handed out": 3.11, 3.12.
[5 Dec] Material covered: 2-SAT applications, SAT and NP (coloring vs SAT).
Exercises "handed out": 3.16 (but c < 2), 3.17, 4.1.
[12 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.
[19 Dec] Material covered: SAT and NP (polynomial reductions, SAT is NP-complete).
Exercises "handed out": None. There are plenty to choose from, if you desire. And perhaps you create your own exercises - this is perhaps the most efficient and creative way of digging into the material.
---(X-mas break)---
[9 Jan] Material covered: Deterministic k-SAT algorithm (Hamming ball search, existence and construction of small covering codes), 3 hrs.
Exercises "handed out": 6.1, 6.2, 6.3, 6.4.
[16 Jan] Material covered: Randomized k-SAT algorithm (local search).
Exercises "handed out": Go through calculations in lecture notes.
[23 Jan] Material covered: Constraint satisfaction
Exercises "handed out": 7.1, 7.2, 7.3.
[30 Jan] Material covered: Random k-CNF formulas
Exercises "handed out": -.
[6 Feb] Material covered: 3 Hrs exercise discussion, no lectures. This is just two weeks before the exam. You can approach Milos before-hand concerning material you would like to be discussed.
Exercises "handed out": -.
---(end of semester)---
Note: The initially announced material of "approximation algorithms and inapproximability results for the MAX-SAT problem" is not covered, for lack of time and since this material is covered in the parallel course on "Approximation: Theory and Algorithms."
[26 Feb] Exam: 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.

Errata:

• Section 0.2, page viii, line -4: ... f_1 and f_2 ... --> ... f and g ...
• Chapter 1, page 9, caption of Figure 1.5: ...`Towards' an equivalent CNF formula we ... --> ... `Towards' f' we ...
• page 19, Exercise 1.21, line 7: ... i.e. a must agree .. --> ... i.e. \alpha must agree ...
• page 23, line +5: ... worth, ... --> ... worse, ...
• Chapter 2, page 25, first paragraph: skip ", and with 8 there is basically one unique example that is not very interesting"
• Chapter 3, page 46, figure with function uc_2s: `Yes' and `No' should be swapped.
• page 61, Exercise 3.16: ... c<3 ... --> ... c<2 ...
• Chapter 4, end of page 69: Part missing, here is the ps-file for it.
• page 72, line + 6, definition of Formula(w): index should be "m=0", not "i=0"

---

Exam: There is a written 2 hours exam that takes place on February 26, 2004 at 10am in HG D3.1, 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 Milos Stojakovic on January 30 or before. (D-INFK students are assumed to have subscribed for the exam through the usual procedures.)

---