Course on

Satisfiability of Boolean Formulas - Combinatorics and Algorithms

Spring 2016

Overview

Course ID: 252-0491-00L
German title: Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
Credits: 7 (3V+2U+1A+1). [more information]
Lecturer: Emo Welzl
Assistant: Chidambaram Annamalai
Time and Location: Tuesdays 10-12 CAB G59 and Thursdays 9-10 CAB G59 (lecture), Tuesday 13-15 CAB G57 (exercise sessions)
Exam: Date and time for the end-of-semester examination is June 2nd 08:00 (sharp!) at CHN F 42.
Language: English

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 sold for 10 Fr. Those who have not yet received a copy please request one from Chillu during the lecture/exercise sessions as we still have copies left. The notes are also available online here (updated February 23, 2016).

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

In the first lecture on Tuesday, February 23, there will be an introduction to course conventions only. The first chapter of the lecture notes will be a self study task. See the table below for a rough schedule. To get an idea have a look at the material covered in lectures in previous years' course web pages.

Three special assignments will be distributed during the semester. The date and time of the final exam is June 2nd 08:00 (sharp!) at CHN F 42.

Week	Date	Material covered	Exercises	Slides and Solutions
8	Tue 23 Feb	Introduction and course conventions. Sections 1.1, 1.2.	Lecture instead of exercises. Sections 1.3, 1.4 were covered. Reading Assignment 1: Basics of Probabilistic Analysis.	--
	Thu 25 Feb	Section 2.1 was covered (till Thm 2.2). Reading Assignment 2: Resolution (Section 1.5)
9	Tue 1 Mar	Lecture Section 2.2, 2.3: Number of Dependent Clauses (LLL without proof) and Partial Satisfaction.	Exercise Session 1 1.3, 1.12, 1.15, 1.18, 1.25, 1.28. Moved to next session: In class: 1.21-1.23. Questions about Reading Assignment 1	Ex. Session 1
	Thu 3 Mar	Exercise Session 2 2.1, 2.2, 2.6. In class: 2.7 Questions about Reading Assignment 1 & 2		Ex. Session 2
10	Tue 8 Mar	Lecture Section 2.3: Partial Satisfaction	Exercise Session 3 2.11, 2.13, 2.15, 2*.1. In class: 2*.3, 2*.4 3.1, 3.3. Section 2.3 Thm 2.7.	Ex. Session 3
	Thu 10 Mar	Lecture Sections 3.1, 3.2: Unit Clause Reduction, Randomized algorithm for 2-SAT
11	Tue 15 Mar	Exercise Session 4 2.3, 2.8, 2.12, 2.14. In Class: 3.2, exercise about resolution.	No exercise session. Special Assignment 1 published on webpage. Solutions to Special Assignment 1.	Ex. Session 4
	Thu 17 Mar	Lecture Sections 3.2.1, 3.2.2: Symmetric Random Walks, Coupling Reading Assignment 3: Coupling
12	Tue 22 Mar	No lecture	Exercise Session 5 3.4, 3.5, 3.8, 3.10, 3.11. In Class: 3.12, 3.13	Ex. Session 5 (updated Mar 30)
	Thu 24 Mar	No lecture
13	Tue 29 Mar	Easter Break
	Thu 31 Mar
14	Tue 5 Apr	Lecture Sections 3.2.2, 3.4.1, 3.4.2, 2*.1. Reading Assignment 4: Linear Time Algorithm for 2-SAT	Lecture instead of exercises. Sections 2*.2, 2*.3, 4.1. Reading Assignment 5: Reduction from 3-SAT to 3-Coloring
	Thu 7 Apr	Lecture Section 4.2: The Class NP and its Relatives.
15	Tue 12 Apr	Lecture Section 4.2: The Class NP and Relatives, Section 5.1. Suggested Reading: Section 4.3 - SAT is NP-Complete.	Exercise Session 6 2*.3, 2*.4, 2*.6, 3.19, 3.20. In Class: 4.1. Special Assignment 2 published on webpage. Solutions to Special Assignment 2.	Ex. Session 6
	Thu 14 Apr	Lecture Section 5.1: Faces of the Cube.
16	Tue 19 Apr	No lecture	Exercise Session 7 4.5, 4.6, 4.7, 4.10, 5.1, 5.4. In Class: 5.8, 5.10.	Ex. Session 7
	Thu 21 Apr	No lecture
17	Tue 26 Apr	Lecture Section 5.2: Hamming Balls. Reading Assignment 6: Proof of Chernoff Bound.	Exercise Session 8 4.9, 5.5, 5.6, 5.7, 5.9, 5.12. In Class: 5.13.	Ex. Session 8
	Thu 28 Apr	Lecture Section 5.2: Covering the Cube with Balls
18	Tue 3 May	Lecture Sections 6.1, 6.2: Coding and k-SAT Algorithms.	Exercise Session 9 5.17, 5.18, 6.1, 6.2, 6.3, 6.4. Special Assignment 3 published on webpage. Solutions to Special Assignment 3.	Ex. Session 9
	Thu 5 May	No lecture (Ascension Day)
19	Tue 10 May	Lecture Section 7.1: A Deterministic Algorithm	Lecture instead of exercises. Section 7.2: A Randomized Algorithm
	Thu 12 May	Lecture Section 8*.1: k-SAT in Subexponential Time?
20	Tue 17 May	Lecture Section 8*.2, 8*.3: The Need for Sparsification, The Sparsification Algorithm.	Exercise Session 10 7.1, 7.2, 7.3. In Class: SAT14 Exam - 1a, 1b, 1d, 3a, 3b, 4a, 4b.	Ex. Session 10
	Thu 19 May	Lecture Section 8*.3: Proof of Point 4 of Theorem 8*.3
21	Tue 24 May	Lecture Section 8*.3: Proof of Point 4 of Theorem 8*.3 Implications of SETH on Orthogonal Vectors problem.	Exercise Session 11 8*.1, 8*.2. In Class: Exercises from SAT15 Exam.	Ex. Session 11
	Thu 26 May	Lecture Section 9: Constraint Satisfaction.
22	Tue 31 May	No lecture. Exercise Session.
	Thu 2 June

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.

  Exam content is all material covered in the lecture, exercises and special assignments.

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

• 30% exercises

  At times in the course of term, we will hand out three 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

The set of exerices for the following week will be listed on this web page every Tuesday. You are encouraged to hand in solutions by the following Tuesday; 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. In addition to the exercises listed beforehand there can be at times in class exercises which will be discussed during the exercise hours. The discussed exercises will be added later to the list on this web page.

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 available here (updated February 23, 2016) along with the exercises that we suggest to be worked through. There is a chance to order the lecture slides as a printed version for 10 Fr.

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

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 | exam pdf | exam ps ]
[7] Course Fall 2009.	[ home page | exam pdf | exam ps ]
[8] Course Fall 2010.	[ home page | exam pdf ]
[9] Course Spring 2012.	[ home page | exam pdf ]
[10] Course Spring 2013.	[ home page | exam pdf ]
[11] Course Spring 2014.	[ home page | exam pdf ]
[12] Course Spring 2015.	[ home page | exam pdf ]