Course on

Satisfiability of Boolean Formulas - Combinatorics and Algorithms

Autumn 2010

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 9-11 CAB G52 (exercise), Friday 11-12 CAB G52 (lecture) TBA
Exam: Wednesday, December 22, 2010
Language: English. If all participants can go along with German, we will switch. The course material will be in English in any case.

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

Primary goals

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

Prerequisites

It is assumed that participants have basic knowledge in propositional logic, probability theory and discrete mathematics as 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).

Course Schedule

Date	Material covered (Presumably to be covered)	Exercises due on that date
Wednesday, September 22	Introduction, motivating examples (circuit verification, map labelling). Conjunctive normal form, polynomial-time conversion of general formulas into SAT-equivalent CNF formulas.	.
Friday, September 24	Notation, formulas and clauses as sets. Algorithm cs for counting. Lecture by Dominik Scheder.	.
Wednesday, September 29	Satisfying assignments, counting satisfying assignments. Extremal properties.	.
Friday, October 1	Dominik gives the lectures. Lovász Local Lemma.	1.9 (generalize to parity over n variables and write a proof that your fellow CS or math student would understand! 1.10 1.11 1.17 1.18
Wednesday, October 6	Partial Satisfaction, Golden Ratio, Proof of Tightness	.
Friday, October 8	Partial Satisfaction of unweighted 2-satisfiable formulas (Käppeli's Theorem)	1.20, 1.21-24 (they are all more all less the same) 1.25, 1.26 2.2, 2.3, 2.6 2.7, 2.8. Hint: First show that 2.8 implies 2.7. Then solve 2.8. Second hint: If you desperately need a hint for 2.8, ask me...
Wednesday, October 13	Polynomial algorithm for 2-SAT; resolution and unit clause reduction; random walk algorithm for 2-SAT; symmetric random walk on Z	First special assignment sheet handed out. Due in class on Wednesday, October 27.
Friday, October 15	2-SAT algorithms; Random walk algorithm; Coupling	2.12 2.13: Somewhat tricky but worth the effort. If you don't know what Hadamard matrices are, ask Dominik. 2.14: Don't write it follows immediately from the definition, because it doesn't. Half of the job is to understand why it's not obvious. 2.15
Wednesday, October 20	Linear algorithm for 2-SAT; algorithmic version of the Lovász Local Lemma. Robin Moser gives the lecture	.
Friday, October 22	Colorability and SAT. Reduction from 3-SAT to 3-Colorability.	Show that there is no weighted 2-satisfiable formula F reaching the 0.618... bound. That is, show that for every particular 2-satisfiable formula, you can do better than Phi = 0.618.... 3.8: Complete the proof of Lemma 3.3, that is, show that e_s is finite and that the equations (3.1) have a unique solution. Let k ≥1 be fixed. For 0 ≤ i ≤ k, let P_i be the probability that the symmetric random walk starting at i reaches k before reaching 0. Derive an explicit formula for P_i and prove it. Clearly, P_0=0 and P_k=1. 3.9. Hint: The previous exercise is helpful! 3.10 3.12
Wednesday, October 27	Polynomial Constant Verifiers, Proof that FP_2 = P.	.
Friday, October 29	Proof that FP_3 = NP.	First special assignment sheet due. 3.17 3.19 3.20
Wednesday, November 3	The cube; faces; Kraft inequality	.
Friday, November 5	Bounds on the volume of Hamming balls	4.2: the one direction is difficult. Try it nevertheless. If you fail, try to prove it for a simpler subcase. I love this exercise 4.5 4.9 Second special assignment handed out (pdf), I corrected a typo on November 10.
Wednesday, November 10	Encoding satisfying assignments. Satisfiability Coding Lemma.	.
Friday, November 12	PPZ algorithm, success probability	5.3 (i.e., reconsider Exercise 2.2) 5.4 5.8 and 5.9 5.10 This is a great exercise. Try not only to obtain a small set, also try to provide a lower bound!
Wednesday, November 17	Deterministic Algorithm for k-SAT using Hamming balls and covering codes	.
Friday, November 19	Schöning's random walk algorithm	Second special assignment due (pdf), I corrected a typo on November 10. 6.2 6.3 6.4
Wednesday, November 24	Schöning's algorithm finished. Dominik starts the chapter on PPSZ, stating the algorithm, definition of forced and guessed variables	.
Friday, November 26	PPSZ algorithm: unique case, clause trees (Dominik gives the lecture)	7.4 (improve algorithm sb from page 105) Third special assignment sheet handed out (pdf)
Wednesday, December 1	PPSZ algorithm: unique case (Dominik gives the lecture)	.
Friday, December 3	One hour exercise, two hours lecture; PPSZ - general case; derandomizing Schöning's algorithm (Dominik gives the lecture)	.
Wednesday, December 8	Constraint Satisfaction	.
Friday, December 10		Third special assignment sheet due (pdf)
Wednesday, December 15		.
Friday, December 17	tba	.
Wednesday, December 22	Exam	.
Friday, December 24	No class. Merry christmas!	.

Exam and grades

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 each grade will account for 10% of your final grade.

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

Regulations for PhD students

For PhD students, the same rules apply for obtaining credit points as for all other participants. Taking the exam and achieving an overall grade of at least 4.0 (computed as a weighted average of grades for special exercises and the written final exam as detailed above) qualifies for receiving credits. In order to comply with new regulations recently issued by the department, merely attending the course and/or handing in exercises is no longer sufficient.

Exercises

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.

What are the "sixth hour" in the Course Catalogue and the seventh credit point supposed to mean?

Apart from three regular lecture (V) hours and two hour of exercises (U), this course comes with one extra sixth hour of independent work (A); this makes 7 credit points. You will deserve the credits for the A-unit by independent work, i.e. studying and learning material (also prerequisistes) on your own. Details will be announced at the beginning of the course the latest.

Lecture Notes

Lecture notes are distributed during the course, including the exercises that we suggest to be worked through. There is no online version of the lecture notes.

Errata

Please check this section for updates on a regular basis. If you discover any mistakes, typos or similar in any of the material we hand out, please advise us as quickly as possible.

where	correction
lecture notes, page 69, second-last paragraph	the sentence since a polynomial k-falsifier can be transformed to a polynomial falsifier F' should be since a polynomial k-falsifier can be transformed to a polynomial verifier F'

Links and Downloads

[1] Course Winter 2003/2004.	[ home page | exam pdf | exam ps ]
[2] Course Winter 2004/2005.	[ home page | exam pdf | exam ps ]
[3] Course Winter 2005/2006.	[ home page | exam pdf | exam ps ]
[4] Course Winter 2006/2007.	[ home page | exam pdf | exam ps ]
[5] Course Winter 2007/2008.	[ home page | exam pdf | exam ps ]
[6] Course Fall 2008.	[ home page | | ]
[6] Course Fall 2009.	[ home page | exam pdf | exam ps ]

last change: June 29 2010 by Dominik Scheder