Department of Computer Science | Institute of Theoretical Computer Science | CADMO

Prof. Emo Welzl and Prof. Bernd Gärtner

Course on

Emo Welzl (lecturer) and Milos Stojakovic (assistant)

Winter 2003, Friday, 10-12 (IFW B42, lectures) and 13-14 (IFW B42, exercises)

Language:

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

[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 "

[26 Feb] Exam: See below.

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