VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.

251-0491-00L 5 Credits BSC , DS , MSC D-MATH , D-INFK
You're viewing possible stale or outdated data. Please check the latest semester for more up-to-date information.

Boolean Satisfiability - Combinatorics and Algorithms

Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen

Lecturers & Examiners: Prof. em. Dr. Emo Welzl
VVZ CR n/a

Last Updated: 2026-02-05 15:14:32

Abstract

Basics (CNF, resolution), extremal properties (probabilistic method, derandomization, Local Lemma, partial satisfaction), 2-SAT algorithms (random walk, implication graph), NP-completeness (Cook-Levin), cube (facial structure, Kraft inequality, Hamming balls, covering codes), SAT algorithms (satisfiability coding lemma, Paturi-Pudlák-Zane, Hamming ball search, Schöning), constraint satisfaction.

Objective

Studying of advanced methods in algorithms design and analysis, and in discrete mathematics along a classical problem in theoretical computer science.

Content

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

Resources

Lecture Notes

There exists no book that covers the many facets of the topic. Lecture notes covering the material of the course will be distributed.

Literature

Here is a list of books with material vaguely 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).

General Information

Language
German
Levels
BSC , DS , MSC
Frequency
Yearly recurring

Examination

Type
end-of-semester examination

Course Components

Type Title Time & Place Hours
lecture Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
  • Fri 10:15-12:00 (CAB G 52)
2 h weekly
exercise Erfüllbarkeit logischer Formeln - Kombinatorik und Algorithmen
  • Fri 13:15-14:00 (CAB G 52)
1 h weekly

Offered In