Satisfiablity (SAT) Course, 2007/08
Course on
Satisfiability of Boolean Formulas - Combinatorics and Algorithms
Herbst 2007 (251-491-00 Erfüllbarkeit logischer Formeln -
Kombinatorik und Algorithmen,
2V1U, 5 credits)
Lecturer: Emo Welzl
Assistant: Dominik Scheder
Time: Friday 10-12 (Lecture), 12-13 (Exercises)
Attention: Time of exercise has changed!
Location: CAB G 52
Schedule: here
Exam: Written exam, Friday, December 21, 10:00 - 12:00.
Language: German, in case nobody expresses preference for English.
All accompanying material will be supplied in 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: Studying of advanced methods in algorithms design
and analysis, and in discrete mathematics along a classical
problem in theoretical computer science.
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).
Previous Years.
web-page course 2003,
web-page course 2004,
web-page course 2005,
web-page course 2006.
Course Schedule
[28 Sep] First lecture. Lecture is extended to the exercises in the afternoon.
Material Covered: basic terminology; circuits, CNF formulas; polynomial-time conversion of circuits into SAT-equivalent CNF formulas
Exercises: 1.3, 1.5, 1.6, 1.7, 1.9, 1.12, 1.17, 1.18
[5 Oct] Lecture will be given by Dominik Scheder.
Material Covered: algorithms for Count-SAT; resolution - correctness and
completeness
Exercises: 1.20, 1.23, 1.25, 1.28, 1.29
[12 Oct] Lecture will be given by Dominik Scheder.
Material Covered: extremal properties (number of clauses/of dependent clauses); partial satisfaction
Exercises: 2.1, 2.2, 2.3, 2.5, 2.6
[19 Oct]
Material Covered: partial satisfaction, unweighted formulas
Exercises: 2.8 (hint: use Hall's Theorem), 2.7 (hint: first do 2.8),
2.13, 2.14 (read 2nd paragraph on page 38), 2.15
[26 Oct]
Material Covered: algorithms for 2-SAT, symmetric random walk
Exercises: 3.1, 3.5, 3.6, 3.11, 3.12, 3.13
[2 Nov]
Material Covered: linear time algorithm for 2-SAT,
algorithms for graph coloring
Exercises: 3.17, 3.18, 3.20, 4.2
[9 Nov]
Material Covered: NP, polynomial constant falsifiers
Exercises: 4.5, 4.10
[16 Nov]
Material Covered: NP = FP3, SAT is NP-complete; the n-dimensional cube; faces
Exercises: 2.3, 4.4, 4.9, 5.1, 5.3, 5.4
[23 Nov]
Material Covered: Hamming balls in the boolean cube; bounds for their volume
Exercises: 5.9, 5.10, 5.11, 5.12
[30 Nov]
Material Covered: Volumes of Hamming balls; covering codes; encoding satisfying
assignments
Exercises: 5.14, 5.16, 5.19
[7 Dec]
Material Covered: PPZ-Algorithm
Exercises: 6.3, 6.4
[14 Dec]
[21 Dec] Exam, 10-12, CAB G 52
Exam: Friday December 21, 2007, 10-12, CAB G 52
Check out previous years exams,
(February 2004
.pdf or
.ps,
February 2005
.pdf or
.ps,
March 2006
.pdf or
.ps),
February 2007
.pdf or
.ps),
See below for further information.
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:
Exam:
There is a written 2 hours exam (exact time and place to be announced),
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.
Time and Location: December 21, 10-12, CAB G 52
Anybody other than D-INFK students should indicate participation in the exam
by email both to Emo Welzl and Dominik Scheder before to be announced.
(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...
