Satisfiablity (SAT) Course, 2003
Satisfiability of Boolean Formulas - Combinatorics and Algorithms
(37-491 Erfüllbarkeit logischer Formeln -
Kombinatorik und Algorithmen,
2V1U, 5 credits)
Winter 2003, Friday, 10-12 (IFW B42, lectures)
and 13-14 (IFW B42, exercises)
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,
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
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.
[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
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 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.
- 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"
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