Course on

Satisfiability of Boolean Formulas - Combinatorics and Algorithms

Spring 2013

Overview

Course ID: 252-0491-00
German title: Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
Credits: 7 (3V+2U+1A+1). [more information]
Lecturer: Emo Welzl
Assistant: Timon Hertli
Time and Location: Tuesday 10-12 CAB G51 (lecture), Friday 9-10 CAB G51 (lecture), Friday 10-12 CAB G51 (exercise)
Exam: Friday, May 31, 9:30-11:30 in ML H 41.1
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 sold for 10 Fr. (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

The lecture starts on Tuesday, February 19. The exercise sessions start on Friday, March 1.

Three special assignments will be distributed during the semester. The final exam is on Friday, May 31.

Week	Date	Material covered	Exercises	Slides and Solutions
8	Tuesday, February 19	Introduction, motivating examples (circuit verification, map labelling). Conjunctive normal form, polynomial-time conversion of general formulas into SAT-equivalent CNF formulas.
	Friday, February 22	Terminology, basic observations	No exercises! Please read the Basics of Probabilistic Analysis.
9	Tuesday, February 26	SAT-counting algorithms, resolution
	Friday, March 1	Formulas with few clauses	1.3, 1.5, 1.6, 1.7, 1.9, 1.12, 1.17, 1.18, 1.19	KW09 Slides
10	Tuesday, March 5	Lovász Local Lemma, partial satisfaction
	Friday, March 8	Partial satisfaction, algorithmic Lovász Local Lemma	Lecture from 9 to 12, exercise session postponed to Tuesday
11	Tuesday, March 12	(exercise session instead of lecture)	inclass exercise about resolution 1.23, 1.25, 1.26, 1.28, 2.2, 2.3, 2.5, 2.6, 2.7	KW10 Slides
	Friday, March 15	2-SAT in polytime using resolution and unit clause reduction	2.9, 2.10, 2.11, 2.12, 2.13, 2.14 inclass exercise about algorithmic Lovász Local Lemma	KW11 Slides
12	Tuesday, March 19	2-SAT in polytime using Papadimitriou's random walk algorithm, 2-SAT in linear time
	Friday, March 22	2-SAT in linear time, applications of 2-SAT to 3-SAT and 3-coloring	Special Assignment 1 is handed out repetition of some aspects of the algorithmic Local Lemma 2*.1, 2*.2, 2*.3 (use n/(8k) instead of n/2^k), 2*.5, 3.1, 3.3, 3.5, 3.6 in-class: 3.8, 3.9, 3.12	KW12 Slides
13	Tuesday, March 26	applications of 2-SAT to 3-SAT and 3-coloring, reduction from coloring to 3-SAT
14	--Easter Break--
15	Tuesday, April 9	reduction from 3-SAT to coloring, verifiers and falsifiers, k-falsifiers
	Friday, April 12	complexity classes, 3-SAT is NP-complete, introduction to the Boolean n-cube	Special Assignment 1 is due this Friday at 23:59 Lecture from 9 to 12, exercise session postponed to Tuesday
16	Tuesday, April 16	(exercise session instead of lecture)	Special Assignment 1 will be discussed	merged with KW16 slides
	Friday, April 19	SAT and the cube, inequalities	Special Assignment 2 will be handed out 3.15, 3.17, 3.19, 3.20, 4.3, 4.4, 4.6, 4.8, 4.9 inclass exercise about polynomial falsifiers	KW16 Slides
17	Tuesday, April 23	Hamming balls
	Friday, April 26	Hamming balls, satisfiability coding and the PPZ algorithm	Lecture from 9 to 12, exercise session postponed to Tuesday
18	Tuesday, April 30	(exercise session instead of lecture)	5.1, 5.4, 5.5, 5.7, 5.9, 5.10, 5.11, 5.12, 5.13, 5.14	KW17 Slides
	Friday, May 3	satisfiability coding and the PPZ algorithm	Special Assignment 2 is due this Friday at 10:15 Special Assignment 2 will be discussed in-class: 6.1	KW18 Slides
19	Tuesday, May 7	Hamming balls and k-SAT algorithms, Schöning's algorithm
	Friday, May 10	Schöning's algorithm	6.2, 6.3, 6.4 (postponed from last week) 7.1, 7.3 in-class exercise about PPZ, in-class exercise about Schöning Special Assignment 3 is handed out	KW19 Slides
20	Tuesday, May 14	The PPSZ Algorithm, Part 1: Basics, Critical Clause Trees
	Friday, May 17	The PPSZ Algorithm, Part 2: Infinite Trees, Finite Trees, Dependent Labels We skip Theorem 8.8, Lemma 8.9, Lemma 8.12 and most of Section 8.2.6.	8.1, 8.2, 8.4 Proof of Theorem 8.10	KW20 Slides
21	Tuesday, May 21	The PPSZ Algorithm, Part 3: Multiple Satisfying Assignment, Cost Function
	Friday, May 24	The PPSZ Algorithm, Part 4: Bounding the Weighted Cost	Special Assignment 3 is due this Friday at 10:15 Discussion of Special Assignment 3
22	Tuesday, May 28	The PPSZ Algorithm, Part 5: Putting Things Together
	Friday, May 31	EXAM from 9:30 to 11:30 in ML H 41.1

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 until and including Friday, May 24.

  Previous exams can be found at [1] through [9] 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

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
Exercise 2.6, page 28	If you are clever, it is indeed possible to use the previous results to solve Exercise 2.6.
Exercise 2.9, page 31	Let A be a set of events,...
Exercise 2*.3, page 44	no more than n/(8k) top-level invocations (instead of n/2^k) This is tight (see KW12 slides for a proof).
All “ Note” paragraphs after Chapter 2.	The numbering is wrong. Note 3.1 should be Note 2*.1 etc.

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 ]