Satisfiability of Boolean Formulas - Combinatorics and Algorithms

Overview

Course ID: 251-0491-00
German title: Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
Credits: 7 (3V+2U+1A+1). [more information]
Lecturer: Emo Welzl
Assistant: Dominik Scheder
Time and Location: Wednesday 8-10, CAB G56 (lecture), Friday 11-12, CAB G52 (lecture), Friday 9-11, CAB G52 (exercises)
Exam: Written exam on Friday, December 18, 2009, 9-11, CAB G52. [more information]
Language: English. If all participants can go along with German, we will switch. The course material will be in English in any case.

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.

• to study advanced methods in algorithms design and analysis and in discrete mathematics along a classical problem in theoretical computer science
• to introduce a number of up-to-date research topics
• to provide basis for independent research on the subject (in a semester/diploma/master/doctoral thesis).

It is assumed that participants have basic knowledge in propositional logic, probability theory and discrete mathematics as supplied in the Vordiplomstudium.

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

Your final grade will be calculated as the the weighted average of:
• 70% final written exam

  The exam is open book, i.e. you are allowed to consult any books, handouts and personal notes of your choice. The use of electronic devices is not allowed.

  Anybody other than D-INFK students should indicate participation in the exam by email both to Emo Welzl and Robin Moser before (deadline to be announced). D-INFK students are expected to subscribe following official procedures.

  Previous exams can be found at [1] through [4] for reference.

• 30% exercises

  At times in the course of term, we will hand out specially marked exercises the solution of which (typeset in LaTeX or similar) is due two weeks later.

  Your solutions will be graded, and your three best grades will account for 10% of your final grade each.

  You are welcome to discuss these exercises with your colleagues, but we expect you to hand in your own writeup.

For PhD students the following rule applies for obtaining credit points (KE) for the course. If you successfully solve (grade 4.0 or better) three out of the four special exercises you get a "Testat" and 4 KE. In order to obtain the remaining 3 KE, you have to take and pass the final exam. No credit points are given for simply sitting in the course.

We will hand out weekly exercises each Friday. You are encouraged to hand in solutions by the following Friday; submitted solutions will be looked at and returned with comments. Note, however, that only the specially marked exercises (see above) will count towards your grade. Nevertheless, we strongly recommend that you solve all weekly problems and attend the exercise classes.